Theorem pm2.61d 180

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  181  pm2.61d2  182  pm5.21ndd  380  bija  381  pm2.61dan  818  ecase3d  1040  ordunidif  6367  dff3  7048  tfindsg  7808  findsg  7844  brtpos  8182  omwordi  8503  omass  8512  nnmwordi  8568  pssnn  9100  frfi  9192  ixpiunwdom  9502  cantnfp1lem3  9599  infxpenlem  9933  infxp  10134  ackbij1lem16  10154  axpowndlem3  10520  pwfseqlem4a  10582  gchina  10620  prlem936  10968  supsrlem  11032  flflp1  13764  hashunx  14346  swrdccat3blem  14699  repswswrd  14744  sumss  15684  fsumss  15685  prodss  15910  fprodss  15911  ruclem2  16197  prmind2  16652  rpexp  16690  fermltl  16752  prmreclem5  16889  ramcl  16998  wunress  17217  divsfval  17509  efgsfo  19712  lt6abl  19868  gsumval3  19880  mdetunilem8  22609  ordtrest2lem  23193  ptpjpre1  23561  fbfinnfr  23831  filufint  23910  ptcmplem2  24043  cphsqrtcl3  25179  ovoliun  25497  voliunlem3  25544  volsup  25548  cxpsqrt  26692  amgm  26979  wilthlem2  27057  sqff1o  27170  chtublem  27199  bposlem1  27272  bposlem3  27274  ostth  27627  nosupbnd1lem1  27697  noinfbnd1lem1  27712  cutlt  27949  clwwisshclwwslemlem  30108  atdmd  32494  atmd2  32496  mdsymlem4  32502  ordtrest2NEWlem  34113  eulerpartlemb  34559  dvelimalcased  35264  dvelimexcased  35266  fineqvac  35304  fineqvnttrclselem1  35309  dfon2lem9  36024  nn0prpwlem  36557  axtcond  36713  bj-ismooredr2  37475  ltflcei  37982  poimirlem30  38024  lplnexllnN  40063  2llnjaN  40065  paddasslem14  40332  cdleme32le  40946  dgrsub2  43587  naddgeoa  43846  evenwodadd  47339  iccelpart  47915  lighneallem3  48092  lighneal  48096