Metamath Proof Explorer


Theorem pm2.24

Description: Theorem *2.24 of WhiteheadRussell p. 104. Its associated inference is pm2.24i . Commuted form of pm2.21 . (Contributed by NM, 3-Jan-2005)

Ref Expression
Assertion pm2.24 φ ¬ φ ψ

Proof

Step Hyp Ref Expression
1 pm2.21 ¬ φ φ ψ
2 1 com12 φ ¬ φ ψ