Metamath Proof Explorer


Theorem pm2.6

Description: Theorem *2.6 of WhiteheadRussell p. 107. (Contributed by NM, 3-Jan-2005)

Ref Expression
Assertion pm2.6 ¬ φ ψ φ ψ ψ

Proof

Step Hyp Ref Expression
1 id ¬ φ ψ ¬ φ ψ
2 idd ¬ φ ψ ψ ψ
3 1 2 jad ¬ φ ψ φ ψ ψ