Theorem pm2.24 125

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

Assertion

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

Proof of Theorem pm2.24

Step	Hyp	Ref	Expression
1		pm2.21 124	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
2	1	com12 33	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  398  orc  880  pm2.82  991  dedlema  1059  cases2ALT  1062  eqneqall  2971  pm2.24nel  3077  preqsnd  4820  ordnbtwn  6445  suppimacnv  8158  ressuppss  8167  ressuppssdif  8169  infssuni  9291  axpowndlem1  10570  ltlen  11299  znnn0nn  12698  elfzonlteqm1  13761  injresinjlem  13810  addmodlteq  13973  ssnn0fi  14012  hasheqf1oi  14378  hashfzp1  14458  swrdnd2  14683  swrdnd0  14685  swrdccat3blem  14766  repswswrd  14811  dvdsaddre2b  16355  dfgcd2  16594  prm23ge5  16865  oddprmdvds  16953  mdegle0  26195  2lgsoddprm  27538  nb3grprlem1  29639  4cyclusnfrgr  30552  broutsideof2  36485  meran1  36784  bj-andnotim  37043  contrd  38608  pell1qrgaplem  43462  clsk1indlem3  44631  pm2.43cbi  45092  afv2orxorb  47820  requad2  48243  zeo2ALTV  48291  ztprmneprm  48978  line2xlem  49384