Introduction to Logic

Or Elimination

Or Elimination is a rule of inference that allows us to derive a conclusion from a disjunction and a set of implications as shown below. If every disjunct appears as the antecedent of one of the implications and every implication has the same consequent, then we can infer the consequent that is shared by all of the implications.

Or Elimination
φ1 ∨ ... ∨ φn
φ1 ⇒ ψ
...
φn ⇒ ψ
ψ