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  2937  pm2.24nel  3043  ralf0  4480  preqsnd  4826  ordnbtwn  6430  suppimacnv  8156  ressuppss  8165  ressuppssdif  8167  infssuni  9304  axpowndlem1  10557  ltlen  11282  znnn0nn  12652  elfzonlteqm1  13709  injresinjlem  13755  addmodlteq  13918  ssnn0fi  13957  hasheqf1oi  14323  hashfzp1  14403  swrdnd2  14627  swrdnd0  14629  swrdccat3blem  14711  repswswrd  14756  dvdsaddre2b  16284  dfgcd2  16523  prm23ge5  16793  oddprmdvds  16881  mdegle0  25989  2lgsoddprm  27334  nb3grprlem1  29314  4cyclusnfrgr  30228  broutsideof2  36117  meran1  36406  bj-andnotim  36583  contrd  38098  pell1qrgaplem  42868  clsk1indlem3  44039  pm2.43cbi  44515  afv2orxorb  47233  requad2  47628  zeo2ALTV  47676  ztprmneprm  48339  line2xlem  48746