Theorem pm2.24 622

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 618	. 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 616

This theorem is referenced by:  pm2.24d  623  pm2.53  723  pm2.82  813  pm4.81dc  909  dedlema  971  alexim  1659  eqneqall  2377  elnelall  2474  sotritric  4360  ltxrlt  8111  zltnle  9391  elfzonlteqm1  10305  qltnle  10352  hashfzp1  10935  dfgcd2  12208  oddprmdvds  12550  2lgsoddprm  15462  bj-fast  15495  nnnotnotr  15744