Theorem pm2.24 624

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

This theorem is referenced by:  pm2.24d  625  pm2.53  727  pm2.82  817  pm4.81dc  913  dedlema  975  ifp2  986  alexim  1691  eqneqall  2410  elnelall  2507  sotritric  4416  ltxrlt  8228  zltnle  9508  elfzonlteqm1  10433  qltnle  10480  hashfzp1  11064  swrdccat3blem  11292  dfgcd2  12556  oddprmdvds  12898  2lgsoddprm  15813  bj-fast  16214  nnnotnotr  16462