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  2412  elnelall  2509  sotritric  4421  ltxrlt  8245  zltnle  9525  elfzonlteqm1  10456  qltnle  10504  hashfzp1  11089  swrdccat3blem  11321  dfgcd2  12587  oddprmdvds  12929  2lgsoddprm  15845  bj-fast  16358  nnnotnotr  16606