Theorem 3eqtr2d 2501

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3eqtr2d.1	|- ( ph -> A = B )
3eqtr2d.2	|- ( ph -> C = B )
3eqtr2d.3	|- ( ph -> C = D )

Assertion

Ref	Expression
3eqtr2d	|- ( ph -> A = D )

Proof of Theorem 3eqtr2d

Step	Hyp	Ref	Expression
1		3eqtr2d.1	. . 3 |- ( ph -> A = B )
2		3eqtr2d.2	. . 3 |- ( ph -> C = B )
3	1, 2	eqtr4d 2498	. 2 |- ( ph -> A = C )
4		3eqtr2d.3	. 2 |- ( ph -> C = D )
5	3, 4	eqtrd 2495	1 |- ( ph -> A = D )

Syntax hints:   -> wi 4   = wceq 1454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-cleq 2454

This theorem is referenced by:  fmptapd  6111  negsub  9947  neg2sub  9959  divmuleq  10339  divneg2  10358  discr  12440  bcpasc  12537  hashgval2  12588  hashf1lem2  12651  relexpaddnn  13162  crim  13226  remullem  13239  incexclem  13942  isum1p  13947  geo2sum  13977  fallfacfwd  14137  fsumkthpow  14157  bpoly3  14159  bpoly4  14160  efi4p  14239  sinhval  14256  addcos  14276  cos2tsin  14281  demoivreALT  14303  rpnnen2lem11  14325  sadaddlem  14488  smumullem  14514  sqgcd  14574  eulerthlem2  14778  vfermltlALT  14801  omeo  14812  pockthlem  14897  4sqlem10  14939  vdwlem2  14980  vdwlem6  14984  vdwlem8  14986  fuccocl  15917  resssetc  16035  resscatc  16048  uncfcurf  16172  yonedalem3b  16212  prdspjmhm  16662  grpinvid2  16763  imasgrp2  16849  lagsubg2  16926  cntzsubm  17037  sylow3lem2  17328  efgredleme  17441  ablsubsub  17508  ablsubsub4  17509  odadd2  17535  gex2abl  17537  pgpfac1lem3a  17757  abvneg  18110  lsppr  18364  psrass1  18677  resspsradd  18688  resspsrvsca  18690  mplcoe5  18740  mplmon2mul  18772  evlslem2  18783  evlsvarsrng  18799  coe1tm  18914  ply1scl1  18933  evls1varsrng  18976  gzrngunit  19081  frlmsubgval  19375  frlmgsum  19378  mamuass  19475  mavmulass  19622  mulmarep1gsum2  19647  mdetuni0  19694  maducoeval2  19713  madulid  19718  mat2pmatmul  19803  decpmatmulsumfsupp  19845  pmatcollpwlem  19852  pm2mpmhmlem1  19890  cmpfi  20471  cnconn  20485  txrest  20694  utopsnneiplem  21310  blcvx  21864  tchcphlem2  22258  minveclem2  22416  minveclem2OLD  22428  pjthlem1  22439  uniioovol  22584  uniioombllem2  22588  uniioombllem2OLD  22589  itg1addlem4  22705  mbfi1fseqlem5  22725  itg2mulc  22753  itg2monolem1  22756  itgaddlem1  22828  itgmulc2lem2  22838  dvrec  22957  lhop2  23015  ftc1lem5  23040  deg1submon1p  23151  plypf1  23214  coefv0  23250  coemulhi  23256  coemulc  23257  dgreq0  23267  dvply1  23285  vieta1  23313  aareccl  23330  aaliou3lem8  23349  dvtaylp  23373  mtest  23407  sineq0  23524  efif1olem2  23540  efif1olem4  23542  tanarg  23616  logtayl2  23655  nnlogbexp  23766  isosctrlem2  23796  chordthmlem2  23807  chordthmlem4  23809  heron  23812  dcubic1lem  23817  dcubic1  23819  mcubic  23821  dquart  23827  quart1lem  23829  quart1  23830  efiasin  23862  asinsin  23866  atancj  23884  efiatan  23886  atanlogaddlem  23887  cosatan  23895  atantan  23897  atans2  23905  log2cnv  23918  log2tlbnd  23919  birthdaylem2  23926  cxplim  23945  lgamgulmlem2  24003  wilthlem1  24041  basellem3  24057  musum  24168  musumsum  24169  muinv  24170  pclogsum  24191  mersenne  24203  dchrabs  24236  dchrinv  24237  lgseisenlem1  24325  lgsquadlem1  24330  lgsquadlem2  24331  lgsquadlem3  24332  lgsquad2lem1  24334  chebbnd1lem3  24357  chpchtlim  24365  rplogsumlem2  24371  dchrisumlem2  24376  dchrmusum2  24380  mulog2sumlem1  24420  mulog2sumlem3  24422  vmalogdivsum2  24424  selberg4lem1  24446  pntrlog2bndlem2  24464  pntrlog2bndlem4  24466  pntibndlem2  24477  pntlemr  24488  pntlemf  24491  pntlemo  24493  ragcom  24791  colperpexlem1  24820  lmiisolem  24886  hypcgrlem2  24890  trgcopyeulem  24895  brbtwn2  24983  colinearalglem1  24984  colinearalglem2  24985  axcontlem2  25043  axcontlem8  25049  clwlkisclwwlklem2a  25561  numclwwlk2  25883  grpoinvid2  26007  gxcom  26045  gxmodid  26055  ablodivdiv4  26067  vcoprne  26246  nvnncan  26332  smcnlem  26381  ipidsq  26397  ipasslem2  26521  minvecolem2  26565  minvecolem2OLD  26575  hv2times  26762  pjhthlem1  27092  pjds3i  27414  ho2times  27520  opsqrlem6  27846  pjclem4  27900  pj3si  27908  csmdsymi  28035  ofoprabco  28315  fcnvgreu  28323  2sqmod  28457  qqhcn  28843  esumpr2  28936  esumpfinval  28944  esumpfinvalf  28945  carsggect  29198  oddpwdcv  29236  eulerpartlemgs2  29261  fibp1  29282  orvcelval  29349  ballotlemscr  29399  ballotlemfrci  29408  ballotlemscrOLD  29437  ballotlemfrciOLD  29446  signsplypnf  29487  subfacp1lem5  29955  cvmliftlem10  30065  circum  30366  faclimlem3  30429  fwddifnp1  30980  bj-bary1lem  31759  tan2h  31981  poimirlem3  31987  poimirlem13  31997  poimirlem14  31998  mblfinlem2  32022  itgaddnclem1  32044  itgmulc2nclem2  32053  areacirclem1  32076  areacirclem4  32079  istotbnd3  32147  iscringd  32276  3atlem1  33092  pmod2iN  33458  polval2N  33515  lhple  33651  cdleme2  33838  cdleme35d  34063  cdleme42h  34093  cdlemeg46ngfr  34129  cdlemkid1  34533  lcfl7lem  35111  mapdpglem22  35305  mapdh6dN  35351  hdmap1l6d  35426  hdmapinvlem3  35535  diophin  35659  irrapxlem2  35711  pellexlem6  35722  pell1234qrmulcl  35745  rmxyval  35807  rmxyneg  35812  rmxyadd  35813  jm2.24  35857  jm2.25  35898  snhesn  36426  radcnvrat  36706  binomcxplemnotnn0  36748  sub2times  37520  mul13d  37526  fperiodmullem  37558  fperiodmul  37559  isumneg  37717  climneg  37726  itgsinexp  37868  stoweidlem13  37910  stoweidlem42  37940  wallispilem4  37967  wallispilem5  37968  wallispi2lem1  37970  stirlinglem1  37973  stirlinglem3  37975  stirlinglem4  37976  stirlinglem5  37977  stirlinglem7  37979  stirlinglem10  37982  dirkertrigeqlem3  37999  fourierdlem30  38036  fourierdlem32  38039  fourierdlem42  38049  fourierdlem42OLD  38050  fourierdlem48  38055  fourierdlem49  38056  fourierdlem83  38090  sqwvfoura  38129  sqwvfourb  38130  etransclem2  38138  etransclem46  38182  sharhght  38511  basvtxval  39163  rngcid  40253  ringcid  40299  lmodvsmdi  40439  dmatALTbas  40466  ldepsprlem  40537  sinhpcosh  40732