Theorem pm2.24 616

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 612	. 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 610

This theorem is referenced by:  pm2.24d  617  pm2.53  717  pm2.82  807  pm4.81dc  903  dedlema  964  alexim  1638  eqneqall  2350  elnelall  2447  sotritric  4309  ltxrlt  7985  zltnle  9258  elfzonlteqm1  10166  qltnle  10202  hashfzp1  10759  dfgcd2  11969  oddprmdvds  12306  bj-fast  13776  nnnotnotr  14025