Theorem pm2.24 611

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 607	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
2	1	com12 30	1 ⊢ (𝜑 → (¬ 𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  pm2.24d  612  pm2.53  712  pm2.82  802  pm4.81dc  894  dedlema  954  alexim  1622  eqneqall  2334  elnelall  2431  sotritric  4279  ltxrlt  7922  zltnle  9192  elfzonlteqm1  10087  qltnle  10123  hashfzp1  10675  dfgcd2  11869  bj-fast  13254