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  4817  ordnbtwn  6420  suppimacnv  8126  ressuppss  8135  ressuppssdif  8137  infssuni  9258  axpowndlem1  10520  ltlen  11246  znnn0nn  12615  elfzonlteqm1  13669  injresinjlem  13718  addmodlteq  13881  ssnn0fi  13920  hasheqf1oi  14286  hashfzp1  14366  swrdnd2  14591  swrdnd0  14593  swrdccat3blem  14674  repswswrd  14719  dvdsaddre2b  16246  dfgcd2  16485  prm23ge5  16755  oddprmdvds  16843  mdegle0  26050  2lgsoddprm  27395  nb3grprlem1  29465  4cyclusnfrgr  30379  broutsideof2  36335  meran1  36624  bj-andnotim  36809  contrd  38342  pell1qrgaplem  43224  clsk1indlem3  44393  pm2.43cbi  44868  afv2orxorb  47582  requad2  47977  zeo2ALTV  48025  ztprmneprm  48701  line2xlem  49107