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  863  pm2.82  972  dedlema  1042  cases2ALT  1045  eqneqall  2953  elnelall  3061  ralf0  4441  preqsnd  4786  ordnbtwn  6341  suppimacnv  7961  ressuppss  7970  ressuppssdif  7972  infssuni  9040  axpowndlem1  10284  ltlen  11006  znnn0nn  12362  elfzonlteqm1  13391  injresinjlem  13435  addmodlteq  13594  ssnn0fi  13633  hasheqf1oi  13994  hashfzp1  14074  swrdnd2  14296  swrdnd0  14298  swrdccat3blem  14380  repswswrd  14425  dvdsaddre2b  15944  dfgcd2  16182  prm23ge5  16444  oddprmdvds  16532  mdegle0  25147  2lgsoddprm  26469  nb3grprlem1  27650  4cyclusnfrgr  28557  broutsideof2  34351  meran1  34527  bj-andnotim  34697  contrd  36182  pell1qrgaplem  40611  clsk1indlem3  41542  pm2.43cbi  42027  afv2orxorb  44607  requad2  44963  zeo2ALTV  45011  ztprmneprm  45571  line2xlem  45987