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  868  pm2.82  978  dedlema  1046  cases2ALT  1049  eqneqall  2944  pm2.24nel  3050  preqsnd  4816  ordnbtwn  6413  suppimacnv  8118  ressuppss  8127  ressuppssdif  8129  infssuni  9250  axpowndlem1  10512  ltlen  11238  znnn0nn  12607  elfzonlteqm1  13661  injresinjlem  13710  addmodlteq  13873  ssnn0fi  13912  hasheqf1oi  14278  hashfzp1  14358  swrdnd2  14583  swrdnd0  14585  swrdccat3blem  14666  repswswrd  14711  dvdsaddre2b  16238  dfgcd2  16477  prm23ge5  16747  oddprmdvds  16835  mdegle0  26042  2lgsoddprm  27387  nb3grprlem1  29436  4cyclusnfrgr  30350  broutsideof2  36297  meran1  36586  bj-andnotim  36763  contrd  38269  pell1qrgaplem  43151  clsk1indlem3  44320  pm2.43cbi  44795  afv2orxorb  47510  requad2  47905  zeo2ALTV  47953  ztprmneprm  48629  line2xlem  49035