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  397  orc  878  pm2.82  988  dedlema  1056  cases2ALT  1059  eqneqall  2967  pm2.24nel  3073  preqsnd  4816  ordnbtwn  6437  suppimacnv  8149  ressuppss  8158  ressuppssdif  8160  infssuni  9286  axpowndlem1  10552  ltlen  11281  znnn0nn  12681  elfzonlteqm1  13744  injresinjlem  13793  addmodlteq  13956  ssnn0fi  13995  hasheqf1oi  14361  hashfzp1  14441  swrdnd2  14666  swrdnd0  14668  swrdccat3blem  14749  repswswrd  14794  dvdsaddre2b  16324  dfgcd2  16563  prm23ge5  16834  oddprmdvds  16922  mdegle0  26117  2lgsoddprm  27457  nb3grprlem1  29527  4cyclusnfrgr  30440  broutsideof2  36436  meran1  36735  bj-andnotim  36995  contrd  38560  pell1qrgaplem  43414  clsk1indlem3  44583  pm2.43cbi  45058  afv2orxorb  47786  requad2  48209  zeo2ALTV  48257  ztprmneprm  48933  line2xlem  49339