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  2950  pm2.24nel  3058  ralf0  4513  preqsnd  4858  ordnbtwn  6476  suppimacnv  8200  ressuppss  8209  ressuppssdif  8211  infssuni  9387  axpowndlem1  10638  ltlen  11363  znnn0nn  12731  elfzonlteqm1  13781  injresinjlem  13827  addmodlteq  13988  ssnn0fi  14027  hasheqf1oi  14391  hashfzp1  14471  swrdnd2  14694  swrdnd0  14696  swrdccat3blem  14778  repswswrd  14823  dvdsaddre2b  16345  dfgcd2  16584  prm23ge5  16854  oddprmdvds  16942  mdegle0  26117  2lgsoddprm  27461  nb3grprlem1  29398  4cyclusnfrgr  30312  broutsideof2  36124  meran1  36413  bj-andnotim  36590  contrd  38105  pell1qrgaplem  42889  clsk1indlem3  44061  pm2.43cbi  44543  afv2orxorb  47245  requad2  47615  zeo2ALTV  47663  ztprmneprm  48268  line2xlem  48679