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  729  pm2.82  819  pm4.81dc  915  dedlema  977  ifp2  988  alexim  1693  eqneqall  2411  elnelall  2508  sotritric  4423  ltxrlt  8250  zltnle  9530  elfzonlteqm1  10461  qltnle  10509  hashfzp1  11094  swrdccat3blem  11329  dfgcd2  12608  oddprmdvds  12950  2lgsoddprm  15871  bj-fast  16398  nnnotnotr  16645