Theorem 3eqtr4d 2220

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

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

Assertion

Ref	Expression
3eqtr4d	|- ( ph -> C = D )

Proof of Theorem 3eqtr4d

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

Syntax hints:   -> wi 4   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  fnsnfv  5577  fvco2  5587  resfunexg  5739  fcof1  5786  fliftfun  5799  caovdir2d  6053  caov32d  6057  caov31d  6059  caov4d  6061  caovlem2d  6069  caofcom  6108  cnvf1olem  6227  tfrlem1  6311  tfrlemisucaccv  6328  tfr1onlemsucaccv  6344  tfrcllemsucaccv  6357  frecrdg  6411  oav2  6466  omv2  6468  omsuc  6475  nnmsucr  6491  ecovicom  6645  ecoviass  6647  ecovidi  6649  nnnninfeq  7128  nninfwlpoimlemg  7175  carden2bex  7190  addcompig  7330  addasspig  7331  mulcompig  7332  mulasspig  7333  distrpig  7334  addassnqg  7383  addnq0mo  7448  mulnq0mo  7449  nqnq0a  7455  nqnq0m  7456  distrnq0  7460  mulcomnq0  7461  addassnq0  7463  addcmpblnr  7740  mulcmpblnrlemg  7741  addsrmo  7744  mulsrmo  7745  ltsrprg  7748  recexgt0sr  7774  mulgt0sr  7779  mulextsr1lem  7781  addcnsrec  7843  mulcnsrec  7844  pitonnlem2  7848  recidpirqlemcalc  7858  axaddcom  7871  adddir  7950  mul32  8089  mul31  8090  add32  8118  add4  8120  sub32  8193  sub4  8204  subdir  8345  mulneg2  8355  mulreim  8563  apadd1  8567  apneg  8570  divassap  8649  divdirap  8656  divmul13ap  8674  divmul24ap  8675  divdiv32ap  8679  conjmulap  8688  zeo  9360  xaddcom  9863  xnegdi  9870  xaddass  9871  xaddass2  9872  xpncan  9873  xadd4d  9887  lincmb01cmp  10005  iccf1o  10006  flhalf  10304  modqvalp1  10345  modqdi  10394  modqsubdir  10395  frecuzrdgg  10418  seq3shft2  10475  seq3caopr3  10483  seq3caopr  10485  seq3f1olemqsumkj  10500  seq3f1olemqsumk  10501  seq3f1olemqsum  10502  seq3homo  10512  seqfeq3  10514  seq3distr  10515  expp1  10529  expnegap0  10530  expaddzaplem  10565  expaddzap  10566  expmulzap  10568  sqneg  10581  sqdivap  10586  subsq2  10630  binom2  10634  modqexp  10649  facp1  10712  bcm1k  10742  bcp1n  10743  bcval5  10745  omgadd  10784  hashun  10787  hashxp  10808  shftfibg  10831  shftfib  10834  shftval  10836  2shfti  10842  seq3shft  10849  crre  10868  remim  10871  mulreap  10875  reneg  10879  readd  10880  remullem  10882  redivap  10885  imneg  10887  imadd  10888  imdivap  10892  cjcj  10894  cjadd  10895  cjmulrcl  10898  cjneg  10901  imval2  10905  resqrexlemcalc1  11025  absneg  11061  sqabsadd  11066  sqabssub  11067  absmul  11080  absresq  11089  absexp  11090  absexpzap  11091  bdtrilem  11249  xrmaxiflemcom  11259  xrmaxadd  11271  xrminrecl  11283  xrminadd  11285  serf0  11362  summodclem3  11390  fsum3  11397  isumss  11401  fisumss  11402  fsumadd  11416  isummulc1  11437  isumdivapc  11438  fsum2dlemstep  11444  fisumcom2  11448  fisum0diag2  11457  fsummulc2  11458  fsummulc1  11459  fsumdivapc  11460  fsumconst  11464  telfsumo  11476  fsumparts  11480  binomlem  11493  isumshft  11500  arisum2  11509  geolim  11521  geo2sum  11524  geo2lim  11526  cvgratnnlemseq  11536  cvgratz  11542  mertenslem2  11546  prodfrecap  11556  prodfdivap  11557  prodmodclem2a  11586  fprodntrivap  11594  fprodssdc  11600  fprodmul  11601  fprodabs  11626  fprod2dlemstep  11632  fprodcom2fi  11636  fprodrec  11639  efcllemp  11668  efcj  11683  efexp  11692  resinval  11725  recosval  11726  cosneg  11737  efival  11742  sinadd  11746  cosadd  11747  addcos  11756  sin2t  11759  cos2t  11760  dvdsmodexp  11804  odd2np1lem  11879  oexpneg  11884  neggcd  11986  gcdabs2  11993  mulgcd  12019  mulgcdr  12021  gcddiv  12022  rplpwr  12030  eucalgval  12056  eucalginv  12058  eucalg  12061  neglcm  12077  lcmgcd  12080  mulgcddvds  12096  qredeu  12099  nn0gcdsq  12202  phimullem  12227  prmdiv  12237  coprimeprodsq  12259  pythagtriplem1  12267  pythagtriplem3  12269  pythagtriplem4  12270  pythagtriplem12  12277  pceulem  12296  pceu  12297  pcqmul  12305  pcexp  12311  pcneg  12326  pcadd  12341  pcmpt  12343  pcmpt2  12344  pcbc  12351  4sqlem7  12384  4sqlem10  12387  mul4sqlem  12393  ennnfonelemp1  12409  setsabsd  12503  setscom  12504  ressbasd  12529  strressid  12532  ressinbasd  12535  ressressg  12536  ressplusgd  12589  imasival  12732  qusin  12751  fvprif  12767  xpsfeq  12769  grpidpropdg  12798  mnd32g  12833  mnd4g  12835  0mhm  12878  mhmco  12879  grpinvcnv  12943  grpinvpropdg  12950  grpinvsub  12957  grpaddsubass  12965  grpsubpropdg  12979  grpsubpropd2  12980  mulgnnp1  12996  mulgnegnn  12998  mulgaddcom  13012  mulginvcom  13013  mulgnndir  13017  mulgnn0ass  13024  mhmmulg  13029  mulgpropdg  13030  subginv  13046  subgsub  13051  subgmulg  13053  eqglact  13089  ablsub4  13121  ablsub32  13130  mgpress  13146  dfur2g  13150  srgass  13159  srgmulgass  13177  srgpcomp  13178  srglmhm  13181  srgrmhm  13182  crngcom  13202  ringass  13204  ringcom  13219  ringsubdi  13238  ringsubdir  13239  mulgass2  13240  opprring  13254  oppr0g  13256  oppr1g  13257  opprnegg  13258  mulgass3  13259  dvdsrvald  13267  unitlinv  13300  unitrinv  13301  dvrfvald  13307  dvrass  13313  dvrdir  13317  rdivmuldivd  13318  rngidpropdg  13320  dvdsrpropdg  13321  unitpropdg  13322  invrpropdg  13323  subrguss  13362  subrginv  13363  subrgdv  13364  lmodcom  13428  lmodsubdir  13440  rmodislmod  13446  tgdom  13611  txbasval  13806  cnmpt11  13822  cnmpt21  13830  setsmsbasg  14018  bdbl  14042  dvmulxxbr  14205  dvimulf  14209  dvcj  14212  dvfre  14213  dvrecap  14216  dvef  14227  sinperlem  14268  coshalfpip  14282  ptolemy  14284  tangtx  14298  relogef  14324  rpcxpadd  14365  rpmulcxp  14369  rpdivcxp  14371  cxpmul  14372  abscxp  14374  rpcxpsqrt  14381  rpabscxpbnd  14398  rplogbreexp  14410  rprelogbmul  14412  rprelogbdiv  14414  lgsneg  14464  lgsmod  14466  lgsdir2  14473  lgsdirprm  14474  lgsdir  14475  lgsdi  14477  lgssq  14480  lgssq2  14481  lgsdirnn0  14487  lgsdinn0  14488  lgseisenlem1  14489  2sqlem3  14503  bj-charfundcALT  14600  nninfsellemeqinf  14804  refeq  14815