Metamath Proof Explorer


Theorem pm2.82

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

Ref Expression
Assertion pm2.82 φψχφ¬χθφψθ

Proof

Step Hyp Ref Expression
1 pm2.24 χ¬χψ
2 1 orim2d χφ¬χφψ
3 2 jao1i φψχφ¬χφψ
4 3 orim1d φψχφ¬χθφψθ