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  395  orc  866  pm2.82  975  dedlema  1045  cases2ALT  1048  eqneqall  2952  pm2.24nel  3060  ralf0  4514  preqsnd  4860  ordnbtwn  6458  suppimacnv  8159  ressuppss  8168  ressuppssdif  8170  infssuni  9343  axpowndlem1  10592  ltlen  11315  znnn0nn  12673  elfzonlteqm1  13708  injresinjlem  13752  addmodlteq  13911  ssnn0fi  13950  hasheqf1oi  14311  hashfzp1  14391  swrdnd2  14605  swrdnd0  14607  swrdccat3blem  14689  repswswrd  14734  dvdsaddre2b  16250  dfgcd2  16488  prm23ge5  16748  oddprmdvds  16836  mdegle0  25595  2lgsoddprm  26919  nb3grprlem1  28637  4cyclusnfrgr  29545  broutsideof2  35094  meran1  35296  bj-andnotim  35466  contrd  36965  pell1qrgaplem  41611  clsk1indlem3  42794  pm2.43cbi  43279  afv2orxorb  45936  requad2  46291  zeo2ALTV  46339  ztprmneprm  47023  line2xlem  47439