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  2972  pm2.24nel  3080  preqsnd  4829  ordnbtwn  6463  suppimacnv  8179  ressuppss  8188  ressuppssdif  8190  infssuni  9313  axpowndlem1  10600  ltlen  11329  znnn0nn  12725  elfzonlteqm1  13789  injresinjlem  13838  addmodlteq  14002  ssnn0fi  14041  hasheqf1oi  14407  hashfzp1  14488  swrdnd2  14717  swrdnd0  14719  swrdccat3blem  14800  repswswrd  14847  dvdsaddre2b  16390  dfgcd2  16629  prm23ge5  16900  oddprmdvds  16988  isfieldidl  21423  mdegle0  26271  2lgsoddprm  27617  nb3grprlem1  29767  4cyclusnfrgr  30680  broutsideof2  36635  meran1  36963  bj-andnotim  37222  contrd  38787  pell1qrgaplem  43641  clsk1indlem3  44810  pm2.43cbi  45268  afv2orxorb  48006  requad2  48429  zeo2ALTV  48477  ztprmneprm  49168  line2xlem  49574