Metamath Proof Explorer


Theorem orel2

Description: Elimination of disjunction by denial of a disjunct. Theorem *2.56 of WhiteheadRussell p. 107. (Contributed by NM, 12-Aug-1994) (Proof shortened by Wolf Lammen, 5-Apr-2013)

Ref Expression
Assertion orel2 ¬φψφψ

Proof

Step Hyp Ref Expression
1 idd ¬φψψ
2 pm2.21 ¬φφψ
3 1 2 jaod ¬φψφψ