Metamath Proof Explorer


Theorem imor

Description: Implication in terms of disjunction. Theorem *4.6 of WhiteheadRussell p. 120. (Contributed by NM, 3-Jan-1993)

Ref Expression
Assertion imor φψ¬φψ

Proof

Step Hyp Ref Expression
1 notnotb φ¬¬φ
2 1 imbi1i φψ¬¬φψ
3 df-or ¬φψ¬¬φψ
4 2 3 bitr4i φψ¬φψ