Theorem 3eqtr2d 2468

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 2465	. 2 |- ( ph -> A = C )
4		3eqtr2d.3	. 2 |- ( ph -> C = D )
5	3, 4	eqtrd 2462	1 |- ( ph -> A = D )

Syntax hints:   -> wi 4   = wceq 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-cleq 2421

This theorem is referenced by:  fmptapd  6047  negsub  9873  neg2sub  9885  divmuleq  10263  divneg2  10282  discr  12359  bcpasc  12456  hashgval2  12507  hashf1lem2  12567  relexpaddnn  13058  crim  13122  remullem  13135  incexclem  13837  isum1p  13842  geo2sum  13872  fallfacfwd  14032  fsumkthpow  14052  bpoly3  14054  bpoly4  14055  efi4p  14134  sinhval  14151  addcos  14171  cos2tsin  14176  demoivreALT  14198  rpnnen2lem11  14220  sadaddlem  14383  smumullem  14409  sqgcd  14469  eulerthlem2  14673  vfermltlALT  14696  omeo  14707  pockthlem  14792  4sqlem10  14834  vdwlem2  14875  vdwlem6  14879  vdwlem8  14881  fuccocl  15812  resssetc  15930  resscatc  15943  uncfcurf  16067  yonedalem3b  16107  prdspjmhm  16557  grpinvid2  16658  imasgrp2  16744  lagsubg2  16821  cntzsubm  16932  sylow3lem2  17223  efgredleme  17336  ablsubsub  17403  ablsubsub4  17404  odadd2  17430  gex2abl  17432  pgpfac1lem3a  17652  abvneg  18005  lsppr  18259  psrass1  18572  resspsradd  18583  resspsrvsca  18585  mplcoe5  18635  mplmon2mul  18667  evlslem2  18678  evlsvarsrng  18694  coe1tm  18809  ply1scl1  18828  evls1varsrng  18871  gzrngunit  18976  frlmsubgval  19269  frlmgsum  19272  mamuass  19369  mavmulass  19516  mulmarep1gsum2  19541  mdetuni0  19588  maducoeval2  19607  madulid  19612  mat2pmatmul  19697  decpmatmulsumfsupp  19739  pmatcollpwlem  19746  pm2mpmhmlem1  19784  cmpfi  20365  cnconn  20379  txrest  20588  utopsnneiplem  21204  blcvx  21758  tchcphlem2  22152  minveclem2  22310  minveclem2OLD  22322  pjthlem1  22333  uniioovol  22478  uniioombllem2  22482  uniioombllem2OLD  22483  itg1addlem4  22599  mbfi1fseqlem5  22619  itg2mulc  22647  itg2monolem1  22650  itgaddlem1  22722  itgmulc2lem2  22732  dvrec  22851  lhop2  22909  ftc1lem5  22934  deg1submon1p  23045  plypf1  23108  coefv0  23144  coemulhi  23150  coemulc  23151  dgreq0  23161  dvply1  23179  vieta1  23207  aareccl  23224  aaliou3lem8  23243  dvtaylp  23267  mtest  23301  sineq0  23418  efif1olem2  23434  efif1olem4  23436  tanarg  23510  logtayl2  23549  nnlogbexp  23660  isosctrlem2  23690  chordthmlem2  23701  chordthmlem4  23703  heron  23706  dcubic1lem  23711  dcubic1  23713  mcubic  23715  dquart  23721  quart1lem  23723  quart1  23724  efiasin  23756  asinsin  23760  atancj  23778  efiatan  23780  atanlogaddlem  23781  cosatan  23789  atantan  23791  atans2  23799  log2cnv  23812  log2tlbnd  23813  birthdaylem2  23820  cxplim  23839  lgamgulmlem2  23897  wilthlem1  23935  basellem3  23951  musum  24062  musumsum  24063  muinv  24064  pclogsum  24085  mersenne  24097  dchrabs  24130  dchrinv  24131  lgseisenlem1  24219  lgsquadlem1  24224  lgsquadlem2  24225  lgsquadlem3  24226  lgsquad2lem1  24228  chebbnd1lem3  24251  chpchtlim  24259  rplogsumlem2  24265  dchrisumlem2  24270  dchrmusum2  24274  mulog2sumlem1  24314  mulog2sumlem3  24316  vmalogdivsum2  24318  selberg4lem1  24340  pntrlog2bndlem2  24358  pntrlog2bndlem4  24360  pntibndlem2  24371  pntlemr  24382  pntlemf  24385  pntlemo  24387  ragcom  24685  colperpexlem1  24714  lmiisolem  24780  hypcgrlem2  24784  trgcopyeulem  24789  brbtwn2  24877  colinearalglem1  24878  colinearalglem2  24879  axcontlem2  24937  axcontlem8  24943  clwlkisclwwlklem2a  25455  numclwwlk2  25777  grpoinvid2  25901  gxcom  25939  gxmodid  25949  ablodivdiv4  25961  vcoprne  26140  nvnncan  26226  smcnlem  26275  ipidsq  26291  ipasslem2  26415  minvecolem2  26459  minvecolem2OLD  26469  hv2times  26656  pjhthlem1  26986  pjds3i  27308  ho2times  27414  opsqrlem6  27740  pjclem4  27794  pj3si  27802  csmdsymi  27929  ofoprabco  28213  fcnvgreu  28221  2sqmod  28360  qqhcn  28747  esumpr2  28840  esumpfinval  28848  esumpfinvalf  28849  carsggect  29102  oddpwdcv  29140  eulerpartlemgs2  29165  fibp1  29186  orvcelval  29253  ballotlemscr  29303  ballotlemfrci  29312  ballotlemscrOLD  29341  ballotlemfrciOLD  29350  signsplypnf  29391  subfacp1lem5  29859  cvmliftlem10  29969  circum  30270  faclimlem3  30332  fwddifnp1  30881  bj-bary1lem  31622  tan2h  31844  poimirlem3  31850  poimirlem13  31860  poimirlem14  31861  mblfinlem2  31885  itgaddnclem1  31907  itgmulc2nclem2  31916  areacirclem1  31939  areacirclem4  31942  istotbnd3  32010  iscringd  32139  3atlem1  32960  pmod2iN  33326  polval2N  33383  lhple  33519  cdleme2  33706  cdleme35d  33931  cdleme42h  33961  cdlemeg46ngfr  33997  cdlemkid1  34401  lcfl7lem  34979  mapdpglem22  35173  mapdh6dN  35219  hdmap1l6d  35294  hdmapinvlem3  35403  diophin  35527  irrapxlem2  35580  pellexlem6  35591  pell1234qrmulcl  35614  rmxyval  35676  rmxyneg  35681  rmxyadd  35682  jm2.24  35726  jm2.25  35767  snhesn  36295  radcnvrat  36576  binomcxplemnotnn0  36618  sub2times  37380  mul13d  37386  fperiodmullem  37418  fperiodmul  37419  isumneg  37563  climneg  37572  itgsinexp  37714  stoweidlem13  37756  stoweidlem42  37786  wallispilem4  37813  wallispilem5  37814  wallispi2lem1  37816  stirlinglem1  37819  stirlinglem3  37821  stirlinglem4  37822  stirlinglem5  37823  stirlinglem7  37825  stirlinglem10  37828  dirkertrigeqlem3  37845  fourierdlem30  37882  fourierdlem32  37885  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem48  37901  fourierdlem49  37902  fourierdlem83  37936  sqwvfoura  37975  sqwvfourb  37976  etransclem2  37984  etransclem46  38028  sharhght  38288  basvtxval  38893  rngcid  39582  ringcid  39628  lmodvsmdi  39770  dmatALTbas  39797  ldepsprlem  39868  sinhpcosh  40063