Theorem pm2.24 120

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

Assertion

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

Proof of Theorem pm2.24

Step	Hyp	Ref	Expression
1		pm2.21 119	. 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  893  dedlema  993  cases2  1005  eqneqall  2793  ordnbtwn  5733  suppimacnv  7193  ressuppss  7201  ressuppssdif  7203  infssuni  8140  axpowndlem1  9298  ltlen  10017  znnn0nn  11365  elfzonlteqm1  12410  injresinjlem  12450  addmodlteq  12607  ssnn0fi  12646  hasheqf1oi  13002  hasheqf1oiOLD  13003  hashfzp1  13078  swrdnd2  13285  swrdccat3blem  13346  repswswrd  13382  dvdsaddre2b  14867  dfgcd2  15101  prm23ge5  15358  oddprmdvds  15445  mdegle0  23641  2lgsoddprm  24941  nb3graprlem1  25980  nbcusgra  25992  wlkdvspthlem  26137  clwwlkprop  26298  hashnbgravdg  26440  4cyclusnfrgra  26546  broutsideof2  31399  meran1  31580  bj-andnotim  31746  contrd  33069  pell1qrgaplem  36455  clsk1indlem3  37361  pm2.43cbi  37745  zeo2ALTV  40120  elnelall  40302  nb3grprlem1  40608  4cyclusnfrgr  41462  ztprmneprm  41918