Theorem pm2.24 124

Description: Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 150. Commuted form of pm2.21 123. (Contributed by NM, 3-Jan-2005.)

Assertion

Ref	Expression
pm2.24	⊢ (𝜑 → (¬ 𝜑 → 𝜓))

Proof of Theorem pm2.24

Step	Hyp	Ref	Expression
1		pm2.21 123	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
2	1	com12 32	1 ⊢ (𝜑 → (¬ 𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm4.81  393  orc  867  pm2.82  977  dedlema  1045  cases2ALT  1048  eqneqall  2940  pm2.24nel  3046  ralf0  4463  preqsnd  4810  ordnbtwn  6406  suppimacnv  8110  ressuppss  8119  ressuppssdif  8121  infssuni  9237  axpowndlem1  10495  ltlen  11221  znnn0nn  12590  elfzonlteqm1  13643  injresinjlem  13692  addmodlteq  13855  ssnn0fi  13894  hasheqf1oi  14260  hashfzp1  14340  swrdnd2  14565  swrdnd0  14567  swrdccat3blem  14648  repswswrd  14693  dvdsaddre2b  16220  dfgcd2  16459  prm23ge5  16729  oddprmdvds  16817  mdegle0  26010  2lgsoddprm  27355  nb3grprlem1  29360  4cyclusnfrgr  30274  broutsideof2  36187  meran1  36476  bj-andnotim  36653  contrd  38157  pell1qrgaplem  42990  clsk1indlem3  44160  pm2.43cbi  44635  afv2orxorb  47352  requad2  47747  zeo2ALTV  47795  ztprmneprm  48471  line2xlem  48878