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  2936  pm2.24nel  3042  ralf0  4467  preqsnd  4813  ordnbtwn  6406  suppimacnv  8114  ressuppss  8123  ressuppssdif  8125  infssuni  9255  axpowndlem1  10510  ltlen  11235  znnn0nn  12605  elfzonlteqm1  13662  injresinjlem  13708  addmodlteq  13871  ssnn0fi  13910  hasheqf1oi  14276  hashfzp1  14356  swrdnd2  14580  swrdnd0  14582  swrdccat3blem  14663  repswswrd  14708  dvdsaddre2b  16236  dfgcd2  16475  prm23ge5  16745  oddprmdvds  16833  mdegle0  25998  2lgsoddprm  27343  nb3grprlem1  29343  4cyclusnfrgr  30254  broutsideof2  36095  meran1  36384  bj-andnotim  36561  contrd  38076  pell1qrgaplem  42846  clsk1indlem3  44016  pm2.43cbi  44492  afv2orxorb  47213  requad2  47608  zeo2ALTV  47656  ztprmneprm  48332  line2xlem  48739