Theorem 3eqtr2d 2476

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

Syntax hints:   -> wi 4   = wceq 1369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2431

This theorem is referenced by:  fmptapd  5897  negsub  9649  neg2sub  9661  divmuleq  10028  divneg2  10047  discr  11993  bcpasc  12089  hashgval2  12133  hashf1lem2  12201  crim  12596  remullem  12609  incexclem  13291  isum1p  13296  geo2sum  13325  efi4p  13413  sinhval  13430  addcos  13450  cos2tsin  13455  demoivreALT  13477  rpnnen2lem11  13499  sadaddlem  13654  smumullem  13680  sqgcd  13734  eulerthlem2  13849  omeo  13873  pockthlem  13958  4sqlem10  14000  vdwlem2  14035  vdwlem6  14039  vdwlem8  14041  fuccocl  14866  resssetc  14952  resscatc  14965  uncfcurf  15041  yonedalem3b  15081  prdspjmhm  15486  grpinvid2  15578  imasgrp2  15661  lagsubg2  15733  cntzsubm  15844  sylow3lem2  16118  efgredleme  16231  ablsubsub  16298  ablsubsub4  16299  odadd2  16322  gex2abl  16324  pgpfac1lem3a  16567  abvneg  16899  lsppr  17154  psrass1  17458  resspsradd  17468  resspsrvsca  17470  mplcoe5  17528  mplcoe2OLD  17530  mplmon2mul  17563  evlslem2  17577  evlsvarsrng  17594  coe1tm  17706  ply1scl1  17724  evls1varsrng  17754  gzrngunit  17858  frlmsubgval  18172  frlmgsumOLD  18175  frlmgsum  18176  mamuass  18286  mavmulass  18340  mulmarep1gsum2  18365  mdetuni0  18407  maducoeval2  18426  madulid  18431  cmpfi  18991  cnconn  19006  txrest  19184  utopsnneiplem  19802  blcvx  20355  tchcphlem2  20731  minveclem2  20893  pjthlem1  20904  uniioovol  21039  uniioombllem2  21043  itg1addlem4  21157  mbfi1fseqlem5  21177  itg2mulc  21205  itg2monolem1  21208  itgaddlem1  21280  itgmulc2lem2  21290  dvrec  21409  lhop2  21467  ftc1lem5  21492  deg1submon1p  21604  plypf1  21660  coefv0  21695  coemulhi  21701  coemulc  21702  dgreq0  21712  dvply1  21730  vieta1  21758  aareccl  21772  aaliou3lem8  21791  dvtaylp  21815  mtest  21849  sineq0  21963  efif1olem2  21979  efif1olem4  21981  tanarg  22048  logtayl2  22087  isosctrlem2  22197  chordthmlem2  22208  chordthmlem4  22210  heron  22213  dcubic1lem  22218  dcubic1  22220  mcubic  22222  dquart  22228  quart1lem  22230  quart1  22231  efiasin  22263  asinsin  22267  atancj  22285  efiatan  22287  atanlogaddlem  22288  cosatan  22296  atantan  22298  atans2  22306  log2cnv  22319  log2tlbnd  22320  birthdaylem2  22326  cxplim  22345  wilthlem1  22386  basellem3  22400  musum  22511  musumsum  22512  muinv  22513  pclogsum  22534  mersenne  22546  dchrabs  22579  dchrinv  22580  lgseisenlem1  22668  lgsquadlem1  22673  lgsquadlem2  22674  lgsquadlem3  22675  lgsquad2lem1  22677  chebbnd1lem3  22700  chpchtlim  22708  rplogsumlem2  22714  dchrisumlem2  22719  dchrmusum2  22723  mulog2sumlem1  22763  mulog2sumlem3  22765  vmalogdivsum2  22767  selberg4lem1  22789  pntrlog2bndlem2  22807  pntrlog2bndlem4  22809  pntibndlem2  22820  pntlemr  22831  pntlemf  22834  pntlemo  22836  ragcom  23069  brbtwn2  23119  colinearalglem1  23120  colinearalglem2  23121  axcontlem2  23179  axcontlem8  23185  grpoinvid2  23686  gxcom  23724  gxmodid  23734  ablodivdiv4  23746  vcoprne  23925  nvnncan  24011  smcnlem  24060  ipidsq  24076  ipasslem2  24200  minvecolem2  24244  hv2times  24431  pjhthlem1  24762  pjds3i  25084  ho2times  25191  opsqrlem6  25517  pjclem4  25571  pj3si  25579  csmdsymi  25706  ofoprabco  25950  fcnvgreu  25959  qqhcn  26389  nnlogbexp  26432  esumpr2  26486  esumpfinval  26493  esumpfinvalf  26494  oddpwdcv  26707  eulerpartlemgs2  26732  fibp1  26753  orvcelval  26820  ballotlemscr  26870  ballotlemfrci  26879  signsplypnf  26920  lgamgulmlem2  26985  subfacp1lem5  27041  cvmliftlem10  27152  fallfacfwd  27508  faclimlem3  27520  fsumkthpow  28168  bpoly3  28170  bpoly4  28171  tan2h  28395  mblfinlem2  28400  itgaddnclem1  28421  itgmulc2nclem2  28430  areacirclem1  28455  areacirclem4  28458  istotbnd3  28641  iscringd  28770  diophin  29082  irrapxlem2  29135  pellexlem6  29146  pell1234qrmulcl  29167  rmxyval  29227  rmxyadd  29233  jm2.24  29277  jm2.25  29319  isumneg  29746  climneg  29754  itgsinexp  29766  stoweidlem13  29779  stoweidlem42  29808  wallispilem4  29834  wallispilem5  29835  wallispi2lem1  29837  stirlinglem1  29840  stirlinglem3  29842  stirlinglem4  29843  stirlinglem5  29844  stirlinglem7  29846  stirlinglem10  29849  sharhght  29872  clwlkisclwwlklem2a  30418  numclwwlk2  30671  lmodvsmdi  30778  ldepsprlem  30937  sinhpcosh  31006  bj-bary1lem  32494  3atlem1  33020  pmod2iN  33386  polval2N  33443  lhple  33579  cdleme2  33765  cdleme35d  33989  cdleme42h  34019  cdlemeg46ngfr  34055  cdlemkid1  34459  lcfl7lem  35037  mapdpglem22  35231  mapdh6dN  35277  hdmap1l6d  35352  hdmapinvlem3  35461