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  2970  pm2.24nel  3078  preqsnd  4817  ordnbtwn  6479  suppimacnv  8222  ressuppss  8231  ressuppssdif  8233  infssuni  9366  axpowndlem1  10712  ltlen  11441  znnn0nn  12840  elfzonlteqm1  13906  injresinjlem  13955  addmodlteq  14119  ssnn0fi  14158  hasheqf1oi  14525  hashfzp1  14606  swrdnd2  14836  swrdnd0  14838  swrdccat3blem  14919  repswswrd  14966  dvdsaddre2b  16509  dfgcd2  16751  prm23ge5  17025  oddprmdvds  17113  isfieldidl  21573  mdegle0  26428  2lgsoddprm  27776  nb3grprlem1  29994  4cyclusnfrgr  30926  mirimanoffr  36640  mirimanofffr  36642  broutsideof2  37078  meran1  37390  bj-andnotim  37649  contrd  39232  pell1qrgaplem  44084  clsk1indlem3  45246  pm2.43cbi  45703  afv2orxorb  48513  requad2  48936  zeo2ALTV  48984  ztprmneprm  49674  line2xlem  50080