Theorem pm2.24 626

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

This theorem is referenced by:  pm2.24d  627  pm2.53  730  pm2.82  820  pm4.81dc  916  dedlema  978  ifp2  989  alexim  1694  eqneqall  2424  elnelall  2521  sotritric  4450  ltxrlt  8355  zltnle  9643  elfzonlteqm1  10580  qltnle  10630  hashfzp1  11217  swrdccat3blem  11459  dfgcd2  12738  oddprmdvds  13080  2lgsoddprm  16115  bj-fast  16652  nnnotnotr  16899