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  28668  4cyclusnfrgr  29576  broutsideof2  35125  meran1  35344  bj-andnotim  35514  contrd  37013  pell1qrgaplem  41659  clsk1indlem3  42842  pm2.43cbi  43327  afv2orxorb  45984  requad2  46339  zeo2ALTV  46387  ztprmneprm  47071  line2xlem  47487