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  4477  preqsnd  4823  ordnbtwn  6427  suppimacnv  8153  ressuppss  8162  ressuppssdif  8164  infssuni  9297  axpowndlem1  10550  ltlen  11275  znnn0nn  12645  elfzonlteqm1  13702  injresinjlem  13748  addmodlteq  13911  ssnn0fi  13950  hasheqf1oi  14316  hashfzp1  14396  swrdnd2  14620  swrdnd0  14622  swrdccat3blem  14704  repswswrd  14749  dvdsaddre2b  16277  dfgcd2  16516  prm23ge5  16786  oddprmdvds  16874  mdegle0  25982  2lgsoddprm  27327  nb3grprlem1  29307  4cyclusnfrgr  30221  broutsideof2  36110  meran1  36399  bj-andnotim  36576  contrd  38091  pell1qrgaplem  42861  clsk1indlem3  44032  pm2.43cbi  44508  afv2orxorb  47229  requad2  47624  zeo2ALTV  47672  ztprmneprm  48335  line2xlem  48742