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  2939  pm2.24nel  3045  ralf0  4464  preqsnd  4811  ordnbtwn  6401  suppimacnv  8104  ressuppss  8113  ressuppssdif  8115  infssuni  9230  axpowndlem1  10485  ltlen  11211  znnn0nn  12581  elfzonlteqm1  13638  injresinjlem  13687  addmodlteq  13850  ssnn0fi  13889  hasheqf1oi  14255  hashfzp1  14335  swrdnd2  14560  swrdnd0  14562  swrdccat3blem  14643  repswswrd  14688  dvdsaddre2b  16215  dfgcd2  16454  prm23ge5  16724  oddprmdvds  16812  mdegle0  26007  2lgsoddprm  27352  nb3grprlem1  29356  4cyclusnfrgr  30267  broutsideof2  36155  meran1  36444  bj-andnotim  36621  contrd  38136  pell1qrgaplem  42905  clsk1indlem3  44075  pm2.43cbi  44550  afv2orxorb  47258  requad2  47653  zeo2ALTV  47701  ztprmneprm  48377  line2xlem  48784