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  398  orc  880  pm2.82  990  dedlema  1060  cases2ALT  1063  eqneqall  2968  pm2.24nel  3076  preqsnd  4823  ordnbtwn  6456  suppimacnv  8168  ressuppss  8177  ressuppssdif  8179  infssuni  9301  axpowndlem1  10588  ltlen  11317  znnn0nn  12713  elfzonlteqm1  13777  injresinjlem  13826  addmodlteq  13989  ssnn0fi  14028  hasheqf1oi  14394  hashfzp1  14475  swrdnd2  14700  swrdnd0  14702  swrdccat3blem  14783  repswswrd  14828  dvdsaddre2b  16371  dfgcd2  16610  prm23ge5  16881  oddprmdvds  16969  isfieldidl  21397  mdegle0  26245  2lgsoddprm  27591  nb3grprlem1  29741  4cyclusnfrgr  30654  broutsideof2  36622  meran1  36950  bj-andnotim  37209  contrd  38774  pell1qrgaplem  43628  clsk1indlem3  44797  pm2.43cbi  45255  afv2orxorb  47993  requad2  48416  zeo2ALTV  48464  ztprmneprm  49155  line2xlem  49561