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  2968  pm2.24nel  3076  preqsnd  4822  ordnbtwn  6457  suppimacnv  8176  ressuppss  8185  ressuppssdif  8187  infssuni  9317  axpowndlem1  10610  ltlen  11339  znnn0nn  12736  elfzonlteqm1  13801  injresinjlem  13850  addmodlteq  14014  ssnn0fi  14053  hasheqf1oi  14419  hashfzp1  14500  swrdnd2  14729  swrdnd0  14731  swrdccat3blem  14812  repswswrd  14859  dvdsaddre2b  16403  dfgcd2  16642  prm23ge5  16913  oddprmdvds  17001  isfieldidl  21455  mdegle0  26309  2lgsoddprm  27660  nb3grprlem1  29848  4cyclusnfrgr  30780  broutsideof2  36710  meran1  37038  bj-andnotim  37297  contrd  38853  pell1qrgaplem  43722  clsk1indlem3  44891  pm2.43cbi  45349  afv2orxorb  48124  requad2  48547  zeo2ALTV  48595  ztprmneprm  49285  line2xlem  49691