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 ( 𝜑 → ( ¬ 𝜑𝜓 ) )