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  393  orc  864  pm2.82  972  dedlema  1042  cases2ALT  1045  eqneqall  2943  pm2.24nel  3051  ralf0  4505  preqsnd  4851  ordnbtwn  6447  suppimacnv  8153  ressuppss  8162  ressuppssdif  8164  infssuni  9339  axpowndlem1  10588  ltlen  11312  znnn0nn  12670  elfzonlteqm1  13705  injresinjlem  13749  addmodlteq  13908  ssnn0fi  13947  hasheqf1oi  14308  hashfzp1  14388  swrdnd2  14602  swrdnd0  14604  swrdccat3blem  14686  repswswrd  14731  dvdsaddre2b  16247  dfgcd2  16485  prm23ge5  16747  oddprmdvds  16835  mdegle0  25935  2lgsoddprm  27265  nb3grprlem1  29106  4cyclusnfrgr  30014  broutsideof2  35589  meran1  35786  bj-andnotim  35956  contrd  37455  pell1qrgaplem  42100  clsk1indlem3  43283  pm2.43cbi  43768  afv2orxorb  46421  requad2  46776  zeo2ALTV  46824  ztprmneprm  47212  line2xlem  47627