Theorem pm2.24 125

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

Assertion

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

Proof of Theorem pm2.24

Step	Hyp	Ref	Expression
1		pm2.21 124	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
2	1	com12 33	1 ⊢ (𝜑 → (¬ 𝜑 → 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm4.81  399  orc  881  pm2.82  991  dedlema  1061  cases2ALT  1064  eqneqall  2967  pm2.24nel  3075  preqsnd  4819  ordnbtwn  6451  suppimacnv  8175  ressuppss  8184  ressuppssdif  8186  infssuni  9319  axpowndlem1  10663  ltlen  11392  znnn0nn  12791  elfzonlteqm1  13856  injresinjlem  13905  addmodlteq  14069  ssnn0fi  14108  hasheqf1oi  14475  hashfzp1  14556  swrdnd2  14785  swrdnd0  14787  swrdccat3blem  14868  repswswrd  14915  dvdsaddre2b  16457  dfgcd2  16699  prm23ge5  16973  oddprmdvds  17061  isfieldidl  21520  mdegle0  26375  2lgsoddprm  27725  nb3grprlem1  29943  4cyclusnfrgr  30875  broutsideof2  36857  meran1  37169  bj-andnotim  37428  contrd  38997  pell1qrgaplem  43833  clsk1indlem3  45002  pm2.43cbi  45460  afv2orxorb  48242  requad2  48665  zeo2ALTV  48713  ztprmneprm  49403  line2xlem  49809