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  2966  pm2.24nel  3074  preqsnd  4813  ordnbtwn  6458  suppimacnv  8194  ressuppss  8203  ressuppssdif  8205  infssuni  9338  axpowndlem1  10685  ltlen  11414  znnn0nn  12813  elfzonlteqm1  13879  injresinjlem  13928  addmodlteq  14092  ssnn0fi  14131  hasheqf1oi  14498  hashfzp1  14579  swrdnd2  14809  swrdnd0  14811  swrdccat3blem  14892  repswswrd  14939  dvdsaddre2b  16482  dfgcd2  16724  prm23ge5  16998  oddprmdvds  17086  isfieldidl  21545  mdegle0  26400  2lgsoddprm  27748  nb3grprlem1  29966  4cyclusnfrgr  30898  mirimanoffr  36546  broutsideof2  36979  meran1  37291  bj-andnotim  37550  contrd  39122  pell1qrgaplem  43973  clsk1indlem3  45136  pm2.43cbi  45594  afv2orxorb  48391  requad2  48814  zeo2ALTV  48862  ztprmneprm  49552  line2xlem  49958