Theorem pm2.61d 179

Description: Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)

Hypotheses

Ref	Expression
pm2.61d.1	⊢ (𝜑 → (𝜓 → 𝜒))
pm2.61d.2	⊢ (𝜑 → (¬ 𝜓 → 𝜒))

Assertion

Ref	Expression
pm2.61d	⊢ (𝜑 → 𝜒)

Proof of Theorem pm2.61d

Step	Hyp	Ref	Expression
1		pm2.61d.2	. . . 4 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
2	1	con1d 145	. . 3 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
3		pm2.61d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	syld 47	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜒))
5	4	pm2.18d 127	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:  pm2.61d1  180  pm2.61d2  181  pm5.21ndd  379  bija  380  pm2.61dan  812  ecase3d  1034  ordunidif  6361  dff3  7039  tfindsg  7797  findsg  7833  brtpos  8171  omwordi  8492  omass  8501  nnmwordi  8556  pssnn  9085  frfi  9176  ixpiunwdom  9483  cantnfp1lem3  9577  infxpenlem  9911  infxp  10112  ackbij1lem16  10132  axpowndlem3  10497  pwfseqlem4a  10559  gchina  10597  prlem936  10945  supsrlem  11009  flflp1  13713  hashunx  14295  swrdccat3blem  14648  repswswrd  14693  sumss  15633  fsumss  15634  prodss  15856  fprodss  15857  ruclem2  16143  prmind2  16598  rpexp  16635  fermltl  16697  prmreclem5  16834  ramcl  16943  wunress  17162  divsfval  17453  efgsfo  19653  lt6abl  19809  gsumval3  19821  mdetunilem8  22535  ordtrest2lem  23119  ptpjpre1  23487  fbfinnfr  23757  filufint  23836  ptcmplem2  23969  cphsqrtcl3  25115  ovoliun  25434  voliunlem3  25481  volsup  25485  cxpsqrt  26640  amgm  26929  wilthlem2  27007  sqff1o  27120  chtublem  27150  bposlem1  27223  bposlem3  27225  ostth  27578  nosupbnd1lem1  27648  noinfbnd1lem1  27663  cutlt  27877  clwwisshclwwslemlem  29995  atdmd  32380  atmd2  32382  mdsymlem4  32388  ordtrest2NEWlem  33956  eulerpartlemb  34402  dvelimalcased  35108  dvelimexcased  35110  fineqvac  35160  fineqvnttrclselem1  35162  dfon2lem9  35854  nn0prpwlem  36387  bj-ismooredr2  37175  ltflcei  37668  poimirlem30  37710  lplnexllnN  39683  2llnjaN  39685  paddasslem14  39952  cdleme32le  40566  dgrsub2  43252  naddgeoa  43511  evenwodadd  47009  iccelpart  47557  lighneallem3  47731  lighneal  47735