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  2949  pm2.24nel  3057  ralf0  4520  preqsnd  4864  ordnbtwn  6479  suppimacnv  8198  ressuppss  8207  ressuppssdif  8209  infssuni  9384  axpowndlem1  10635  ltlen  11360  znnn0nn  12727  elfzonlteqm1  13777  injresinjlem  13823  addmodlteq  13984  ssnn0fi  14023  hasheqf1oi  14387  hashfzp1  14467  swrdnd2  14690  swrdnd0  14692  swrdccat3blem  14774  repswswrd  14819  dvdsaddre2b  16341  dfgcd2  16580  prm23ge5  16849  oddprmdvds  16937  mdegle0  26131  2lgsoddprm  27475  nb3grprlem1  29412  4cyclusnfrgr  30321  broutsideof2  36104  meran1  36394  bj-andnotim  36571  contrd  38084  pell1qrgaplem  42861  clsk1indlem3  44033  pm2.43cbi  44516  afv2orxorb  47178  requad2  47548  zeo2ALTV  47596  ztprmneprm  48192  line2xlem  48603