Theorem pm2.24 124

Description: Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 150. Commuted form of pm2.21 123. (Contributed by NM, 3-Jan-2005.)

Assertion

Ref	Expression
pm2.24	⊢ (𝜑 → (¬ 𝜑 → 𝜓))

Proof of Theorem pm2.24

Step	Hyp	Ref	Expression
1		pm2.21 123	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
2	1	com12 32	1 ⊢ (𝜑 → (¬ 𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm4.81  394  orc  865  pm2.82  974  dedlema  1044  cases2ALT  1047  eqneqall  2951  pm2.24nel  3059  ralf0  4512  preqsnd  4858  ordnbtwn  6454  suppimacnv  8155  ressuppss  8164  ressuppssdif  8166  infssuni  9339  axpowndlem1  10588  ltlen  11311  znnn0nn  12669  elfzonlteqm1  13704  injresinjlem  13748  addmodlteq  13907  ssnn0fi  13946  hasheqf1oi  14307  hashfzp1  14387  swrdnd2  14601  swrdnd0  14603  swrdccat3blem  14685  repswswrd  14730  dvdsaddre2b  16246  dfgcd2  16484  prm23ge5  16744  oddprmdvds  16832  mdegle0  25586  2lgsoddprm  26908  nb3grprlem1  28626  4cyclusnfrgr  29534  broutsideof2  35082  meran1  35284  bj-andnotim  35454  contrd  36953  pell1qrgaplem  41596  clsk1indlem3  42779  pm2.43cbi  43264  afv2orxorb  45922  requad2  46277  zeo2ALTV  46325  ztprmneprm  46976  line2xlem  47392