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  873  pm2.82  983  dedlema  1051  cases2ALT  1054  eqneqall  2946  pm2.24nel  3052  preqsnd  4797  ordnbtwn  6412  suppimacnv  8121  ressuppss  8130  ressuppssdif  8132  infssuni  9253  axpowndlem1  10518  ltlen  11245  znnn0nn  12638  elfzonlteqm1  13694  injresinjlem  13743  addmodlteq  13906  ssnn0fi  13945  hasheqf1oi  14311  hashfzp1  14391  swrdnd2  14616  swrdnd0  14618  swrdccat3blem  14699  repswswrd  14744  dvdsaddre2b  16274  dfgcd2  16513  prm23ge5  16784  oddprmdvds  16872  mdegle0  26067  2lgsoddprm  27404  nb3grprlem1  29474  4cyclusnfrgr  30387  broutsideof2  36357  meran1  36646  bj-andnotim  36906  contrd  38471  pell1qrgaplem  43325  clsk1indlem3  44494  pm2.43cbi  44969  afv2orxorb  47698  requad2  48121  zeo2ALTV  48169  ztprmneprm  48845  line2xlem  49251