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  898  dedlema  959  alexim  1633  eqneqall  2346  elnelall  2443  sotritric  4302  ltxrlt  7964  zltnle  9237  elfzonlteqm1  10145  qltnle  10181  hashfzp1  10737  dfgcd2  11947  oddprmdvds  12284  bj-fast  13622  nnnotnotr  13872