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 ¬φψφψψ