Metamath Proof Explorer


Theorem pm4.43

Description: Theorem *4.43 of WhiteheadRussell p. 119. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 26-Nov-2012)

Ref Expression
Assertion pm4.43 φ φ ψ φ ¬ ψ

Proof

Step Hyp Ref Expression
1 pm3.24 ¬ ψ ¬ ψ
2 1 biorfi φ φ ψ ¬ ψ
3 ordi φ ψ ¬ ψ φ ψ φ ¬ ψ
4 2 3 bitri φ φ ψ φ ¬ ψ