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  867  pm2.82  977  dedlema  1045  cases2ALT  1048  eqneqall  2944  pm2.24nel  3050  ralf0  4494  preqsnd  4840  ordnbtwn  6452  suppimacnv  8178  ressuppss  8187  ressuppssdif  8189  infssuni  9363  axpowndlem1  10616  ltlen  11341  znnn0nn  12709  elfzonlteqm1  13762  injresinjlem  13808  addmodlteq  13969  ssnn0fi  14008  hasheqf1oi  14374  hashfzp1  14454  swrdnd2  14678  swrdnd0  14680  swrdccat3blem  14762  repswswrd  14807  dvdsaddre2b  16331  dfgcd2  16570  prm23ge5  16840  oddprmdvds  16928  mdegle0  26039  2lgsoddprm  27384  nb3grprlem1  29364  4cyclusnfrgr  30278  broutsideof2  36145  meran1  36434  bj-andnotim  36611  contrd  38126  pell1qrgaplem  42871  clsk1indlem3  44042  pm2.43cbi  44518  afv2orxorb  47237  requad2  47617  zeo2ALTV  47665  ztprmneprm  48302  line2xlem  48713