Theorem pm2.24 593

Description: Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)

Assertion

Ref	Expression
pm2.24	⊢ (𝜑 → (¬ 𝜑 → 𝜓))

Proof of Theorem pm2.24

Step	Hyp	Ref	Expression
1		pm2.21 589	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
2	1	com12 30	1 ⊢ (𝜑 → (¬ 𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in2 587

This theorem is referenced by:  pm2.24d  594  pm2.53  694  pm2.82  784  pm4.81dc  876  dedlema  936  alexim  1607  eqneqall  2292  elnelall  2389  sotritric  4206  ltxrlt  7754  zltnle  9004  elfzonlteqm1  9880  qltnle  9916  hashfzp1  10463  dfgcd2  11548  bj-fast  12645