Introduction to Logic

Implication Elimination

Implication Elimination is a rule of inference that allows us to deduce the consequent of an implication from that implication and its antecedent.

Implication Elimination
φ ⇒ ψ
φ
ψ