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  2943  pm2.24nel  3049  preqsnd  4815  ordnbtwn  6412  suppimacnv  8116  ressuppss  8125  ressuppssdif  8127  infssuni  9246  axpowndlem1  10508  ltlen  11234  znnn0nn  12603  elfzonlteqm1  13657  injresinjlem  13706  addmodlteq  13869  ssnn0fi  13908  hasheqf1oi  14274  hashfzp1  14354  swrdnd2  14579  swrdnd0  14581  swrdccat3blem  14662  repswswrd  14707  dvdsaddre2b  16234  dfgcd2  16473  prm23ge5  16743  oddprmdvds  16831  mdegle0  26038  2lgsoddprm  27383  nb3grprlem1  29453  4cyclusnfrgr  30367  broutsideof2  36316  meran1  36605  bj-andnotim  36788  contrd  38294  pell1qrgaplem  43111  clsk1indlem3  44280  pm2.43cbi  44755  afv2orxorb  47470  requad2  47865  zeo2ALTV  47913  ztprmneprm  48589  line2xlem  48995