Theorem pm2.24 124

Description: Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 153. 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  397  orc  864  pm2.82  973  dedlema  1041  cases2ALT  1044  eqneqall  2998  elnelall  3104  ordnbtwn  6249  suppimacnv  7824  ressuppss  7832  ressuppssdif  7834  infssuni  8799  axpowndlem1  10008  ltlen  10730  znnn0nn  12082  elfzonlteqm1  13108  injresinjlem  13152  addmodlteq  13309  ssnn0fi  13348  hasheqf1oi  13708  hashfzp1  13788  swrdnd2  14008  swrdnd0  14010  swrdccat3blem  14092  repswswrd  14137  dvdsaddre2b  15649  dfgcd2  15884  prm23ge5  16142  oddprmdvds  16229  mdegle0  24678  2lgsoddprm  26000  nb3grprlem1  27170  4cyclusnfrgr  28077  broutsideof2  33696  meran1  33872  bj-andnotim  34035  contrd  35535  pell1qrgaplem  39814  clsk1indlem3  40746  pm2.43cbi  41224  afv2orxorb  43784  requad2  44141  zeo2ALTV  44189  ztprmneprm  44749  line2xlem  45167