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  866  pm2.82  976  dedlema  1046  cases2ALT  1049  eqneqall  2957  pm2.24nel  3065  ralf0  4537  preqsnd  4883  ordnbtwn  6488  suppimacnv  8215  ressuppss  8224  ressuppssdif  8226  infssuni  9414  axpowndlem1  10666  ltlen  11391  znnn0nn  12754  elfzonlteqm1  13792  injresinjlem  13837  addmodlteq  13997  ssnn0fi  14036  hasheqf1oi  14400  hashfzp1  14480  swrdnd2  14703  swrdnd0  14705  swrdccat3blem  14787  repswswrd  14832  dvdsaddre2b  16355  dfgcd2  16593  prm23ge5  16862  oddprmdvds  16950  mdegle0  26136  2lgsoddprm  27478  nb3grprlem1  29415  4cyclusnfrgr  30324  broutsideof2  36086  meran1  36377  bj-andnotim  36554  contrd  38057  pell1qrgaplem  42829  clsk1indlem3  44005  pm2.43cbi  44489  afv2orxorb  47143  requad2  47497  zeo2ALTV  47545  ztprmneprm  48072  line2xlem  48487