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  726  pm2.82  816  pm4.81dc  912  dedlema  974  alexim  1671  eqneqall  2390  elnelall  2487  sotritric  4392  ltxrlt  8180  zltnle  9460  elfzonlteqm1  10383  qltnle  10430  hashfzp1  11013  swrdccat3blem  11237  dfgcd2  12501  oddprmdvds  12843  2lgsoddprm  15757  bj-fast  16015  nnnotnotr  16263