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  2422  elnelall  2519  sotritric  4444  ltxrlt  8335  zltnle  9619  elfzonlteqm1  10551  qltnle  10599  hashfzp1  11184  swrdccat3blem  11424  dfgcd2  12703  oddprmdvds  13045  2lgsoddprm  15973  bj-fast  16500  nnnotnotr  16747