Theorem pm2.24 121

Description: Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 146. (Contributed by NM, 3-Jan-2005.)

Assertion

Ref	Expression
pm2.24	⊢ (𝜑 → (¬ 𝜑 → 𝜓))

Proof of Theorem pm2.24

Step	Hyp	Ref	Expression
1		pm2.21 120	. 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  380  orc  399  pm2.82  915  dedlema  1014  cases2ALT  1017  eqneqall  2834  elnelall  2939  ordnbtwn  5854  suppimacnv  7351  ressuppss  7359  ressuppssdif  7361  infssuni  8298  axpowndlem1  9457  ltlen  10176  znnn0nn  11527  elfzonlteqm1  12583  injresinjlem  12628  addmodlteq  12785  ssnn0fi  12824  hasheqf1oi  13180  hashfzp1  13256  swrdnd2  13479  swrdccat3blem  13541  repswswrd  13577  dvdsaddre2b  15076  dfgcd2  15310  prm23ge5  15567  oddprmdvds  15654  mdegle0  23882  2lgsoddprm  25186  nb3grprlem1  26326  4cyclusnfrgr  27272  broutsideof2  32354  meran1  32535  bj-andnotim  32698  contrd  34029  pell1qrgaplem  37754  clsk1indlem3  38658  pm2.43cbi  39041  zeo2ALTV  41907  ztprmneprm  42450