Theorem pm2.24 621

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 617	. 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 615

This theorem is referenced by:  pm2.24d  622  pm2.53  722  pm2.82  812  pm4.81dc  908  dedlema  969  alexim  1643  eqneqall  2355  elnelall  2452  sotritric  4318  ltxrlt  7997  zltnle  9272  elfzonlteqm1  10180  qltnle  10216  hashfzp1  10772  dfgcd2  11982  oddprmdvds  12319  bj-fast  14053  nnnotnotr  14302