Theorem pm2.24 622

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

This theorem is referenced by:  pm2.24d  623  pm2.53  724  pm2.82  814  pm4.81dc  910  dedlema  972  alexim  1669  eqneqall  2387  elnelall  2484  sotritric  4375  ltxrlt  8145  zltnle  9425  elfzonlteqm1  10346  qltnle  10393  hashfzp1  10976  dfgcd2  12379  oddprmdvds  12721  2lgsoddprm  15634  bj-fast  15751  nnnotnotr  16000