肯定前件

条件式 $P\to Q$ 承诺：一旦前件 $P$ 成立，后件 $Q$ 就可使用。肯定前件把“条件已经满足”与这份承诺结合起来，消去蕴含符号，得到实际结论。

它也是函数应用的逻辑原型。在 Curry–Howard 对应下，$P\to Q$ 的证明可以看成把 $P$ 的证明转换为 $Q$ 的证明的函数；给定一个 $P$ 的证明后，应用该函数便得到 $Q$。自然演绎因此把肯定前件称为蕴含消去。

规则可靠不等于其逆向推理可靠。$Q$ 可能由许多不同原因成立，所以从 $P\to Q$ 与 $Q$ 不能恢复 $P$。同样，前件为假时材料蕴含仍为真，不能从 $P\to Q$ 与 $\mathrm{\neg }P$ 推出 $\mathrm{\neg }Q$。

若已知“一个整数是 $6$ 的倍数，则它是偶数”，并且已经证明 $n$ 是 $6$ 的倍数，就可推出 $n$ 是偶数。这里前提与条件式左侧完全一致，规则可以直接应用。

若只知道 $n$ 是偶数，则不能反推 $n$ 是 $6$ 的倍数；这是肯定后件。若知道 $n$ 不是 $6$ 的倍数，也不能推出它不是偶数；这是拒斥前件。二者都把单向条件误当成双向等价。

实际证明中，前件可能只在逻辑等价意义下匹配。例如已有 $P\wedge R$，而条件式需要 $P$。此时必须先用合取消去得到 $P$，再应用肯定前件。证明检查器不会把“语义上差不多”自动视为同一公式，所有变形都需要合法规则支持。

在经典逻辑中，对置推理

是有效的，但它是拒取式而非肯定前件。区分这些模式可以避免只凭自然语言语气判断推理方向。

演绎定理公理库演绎定理Deduction theorem在适当证明系统中，把一个临时前提移入蕴含式前件。把临时前提移入蕴含前件，肯定前件则把已满足的前件从蕴含中消去。两者在 Hilbert 系统中形成“引入条件—使用条件”的基本往返。

在类型论中，箭头类型的消去规则就是函数应用；在程序验证中，已经证明的前置条件与规格蕴含结合后给出后置事实；在逻辑编程与规则系统中，匹配规则前件并触发结论也是同一结构。具体系统可能加入资源、时态或模态限制，但核心仍是：只有当前件确实建立后，才能使用条件式给出的结论。