Theorem 3eqtr2d 2471

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

Syntax hints:   -> wi 4   = wceq 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-ex 1590  df-cleq 2426

This theorem is referenced by:  fmptapd  5889  negsub  9644  neg2sub  9656  divmuleq  10023  divneg2  10042  discr  11984  bcpasc  12080  hashgval2  12124  hashf1lem2  12192  crim  12587  remullem  12600  incexclem  13281  isum1p  13286  geo2sum  13315  efi4p  13403  sinhval  13420  addcos  13440  cos2tsin  13445  demoivreALT  13467  rpnnen2lem11  13489  sadaddlem  13644  smumullem  13670  sqgcd  13724  eulerthlem2  13839  omeo  13863  pockthlem  13948  4sqlem10  13990  vdwlem2  14025  vdwlem6  14029  vdwlem8  14031  fuccocl  14856  resssetc  14942  resscatc  14955  uncfcurf  15031  yonedalem3b  15071  prdspjmhm  15476  grpinvid2  15566  imasgrp2  15649  lagsubg2  15721  cntzsubm  15832  sylow3lem2  16106  efgredleme  16219  ablsubsub  16286  ablsubsub4  16287  odadd2  16310  gex2abl  16312  pgpfac1lem3a  16550  abvneg  16842  lsppr  17095  psrass1  17411  resspsradd  17421  resspsrvsca  17423  mplcoe2  17480  mplcoe2OLD  17481  mplmon2mul  17514  evlslem2  17524  coe1tm  17623  ply1scl1  17641  gzrngunit  17721  frlmsubgval  18033  frlmgsumOLD  18036  frlmgsum  18037  mamuass  18147  mavmulass  18201  mulmarep1gsum2  18226  mdetuni0  18268  maducoeval2  18287  madulid  18292  cmpfi  18852  cnconn  18867  txrest  19045  utopsnneiplem  19663  blcvx  20216  tchcphlem2  20592  minveclem2  20754  pjthlem1  20765  uniioovol  20900  uniioombllem2  20904  itg1addlem4  21018  mbfi1fseqlem5  21038  itg2mulc  21066  itg2monolem1  21069  itgaddlem1  21141  itgmulc2lem2  21151  dvrec  21270  lhop2  21328  ftc1lem5  21353  deg1submon1p  21508  plypf1  21564  coefv0  21599  coemulhi  21605  coemulc  21606  dgreq0  21616  dvply1  21634  vieta1  21662  aareccl  21676  aaliou3lem8  21695  dvtaylp  21719  mtest  21753  sineq0  21867  efif1olem2  21883  efif1olem4  21885  tanarg  21952  logtayl2  21991  isosctrlem2  22101  chordthmlem2  22112  chordthmlem4  22114  heron  22117  dcubic1lem  22122  dcubic1  22124  mcubic  22126  dquart  22132  quart1lem  22134  quart1  22135  efiasin  22167  asinsin  22171  atancj  22189  efiatan  22191  atanlogaddlem  22192  cosatan  22200  atantan  22202  atans2  22210  log2cnv  22223  log2tlbnd  22224  birthdaylem2  22230  cxplim  22249  wilthlem1  22290  basellem3  22304  musum  22415  musumsum  22416  muinv  22417  pclogsum  22438  mersenne  22450  dchrabs  22483  dchrinv  22484  lgseisenlem1  22572  lgsquadlem1  22577  lgsquadlem2  22578  lgsquadlem3  22579  lgsquad2lem1  22581  chebbnd1lem3  22604  chpchtlim  22612  rplogsumlem2  22618  dchrisumlem2  22623  dchrmusum2  22627  mulog2sumlem1  22667  mulog2sumlem3  22669  vmalogdivsum2  22671  selberg4lem1  22693  pntrlog2bndlem2  22711  pntrlog2bndlem4  22713  pntibndlem2  22724  pntlemr  22735  pntlemf  22738  pntlemo  22740  brbtwn2  22973  colinearalglem1  22974  colinearalglem2  22975  axcontlem2  23033  axcontlem8  23039  grpoinvid2  23540  gxcom  23578  gxmodid  23588  ablodivdiv4  23600  vcoprne  23779  nvnncan  23865  smcnlem  23914  ipidsq  23930  ipasslem2  24054  minvecolem2  24098  hv2times  24285  pjhthlem1  24616  pjds3i  24938  ho2times  25045  opsqrlem6  25371  pjclem4  25425  pj3si  25433  csmdsymi  25560  ofoprabco  25805  fcnvgreu  25814  qqhcn  26273  nnlogbexp  26316  esumpr2  26370  esumpfinval  26377  esumpfinvalf  26378  oddpwdcv  26585  eulerpartlemgs2  26610  fibp1  26631  orvcelval  26698  ballotlemscr  26748  ballotlemfrci  26757  signsplypnf  26798  lgamgulmlem2  26863  subfacp1lem5  26919  cvmliftlem10  27030  fallfacfwd  27385  faclimlem3  27397  fsumkthpow  28045  bpoly3  28047  bpoly4  28048  tan2h  28265  mblfinlem2  28270  itgaddnclem1  28291  itgmulc2nclem2  28300  areacirclem1  28325  areacirclem4  28328  istotbnd3  28511  iscringd  28640  diophin  28953  irrapxlem2  29006  pellexlem6  29017  pell1234qrmulcl  29038  rmxyval  29098  rmxyadd  29104  jm2.24  29148  jm2.25  29190  isumneg  29618  climneg  29626  itgsinexp  29638  stoweidlem13  29651  stoweidlem42  29680  wallispilem4  29706  wallispilem5  29707  wallispi2lem1  29709  stirlinglem1  29712  stirlinglem3  29714  stirlinglem4  29715  stirlinglem5  29716  stirlinglem7  29718  stirlinglem10  29721  sharhght  29744  clwlkisclwwlklem2a  30290  numclwwlk2  30543  ldepsprlem  30712  sinhpcosh  30781  bj-bary1lem  32171  3atlem1  32697  pmod2iN  33063  polval2N  33120  lhple  33256  cdleme2  33442  cdleme35d  33666  cdleme42h  33696  cdlemeg46ngfr  33732  cdlemkid1  34136  lcfl7lem  34714  mapdpglem22  34908  mapdh6dN  34954  hdmap1l6d  35029  hdmapinvlem3  35138