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  868  pm2.82  978  dedlema  1046  cases2ALT  1049  eqneqall  2944  pm2.24nel  3050  preqsnd  4803  ordnbtwn  6412  suppimacnv  8117  ressuppss  8126  ressuppssdif  8128  infssuni  9249  axpowndlem1  10511  ltlen  11238  znnn0nn  12631  elfzonlteqm1  13687  injresinjlem  13736  addmodlteq  13899  ssnn0fi  13938  hasheqf1oi  14304  hashfzp1  14384  swrdnd2  14609  swrdnd0  14611  swrdccat3blem  14692  repswswrd  14737  dvdsaddre2b  16267  dfgcd2  16506  prm23ge5  16777  oddprmdvds  16865  mdegle0  26052  2lgsoddprm  27393  nb3grprlem1  29463  4cyclusnfrgr  30377  broutsideof2  36320  meran1  36609  bj-andnotim  36869  contrd  38432  pell1qrgaplem  43319  clsk1indlem3  44488  pm2.43cbi  44963  afv2orxorb  47688  requad2  48111  zeo2ALTV  48159  ztprmneprm  48835  line2xlem  49241