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  4445  ltxrlt  8339  zltnle  9623  elfzonlteqm1  10555  qltnle  10603  hashfzp1  11189  swrdccat3blem  11429  dfgcd2  12708  oddprmdvds  13050  2lgsoddprm  15984  bj-fast  16511  nnnotnotr  16758