Theorem pm2.24 630

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 626	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
2	1	com12 30	1 ⊢ (𝜑 → (¬ 𝜑 → 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 624

This theorem is used by:  pm2.24d  631  pm2.53  734  pm2.82  824  pm4.81dc  920  dedlema  982  ifp2  993  alexim  1698  eqneqall  2430  elnelall  2527  sotritric  4471  ltxrlt  8398  zltnle  9702  elfzonlteqm1  10646  qltnle  10696  hashfzp1  11288  swrdccat3blem  11534  dfgcd2  12817  oddprmdvds  13163  2lgsoddprm  16449  bj-fast  16986  nnnotnotr  17233