Theorem 3eqtr4d 2230

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 2223	. 2 |- ( ph -> D = A )
5	1, 4	eqtr4d 2223	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1363

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 1457  ax-gen 1459  ax-4 1520  ax-17 1536  ax-ext 2169

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

This theorem is referenced by:  fnsnfv  5588  fvco2  5598  resfunexg  5750  fcof1  5797  fliftfun  5810  caovdir2d  6065  caov32d  6069  caov31d  6071  caov4d  6073  caovlem2d  6081  caofcom  6120  cnvf1olem  6239  tfrlem1  6323  tfrlemisucaccv  6340  tfr1onlemsucaccv  6356  tfrcllemsucaccv  6369  frecrdg  6423  oav2  6478  omv2  6480  omsuc  6487  nnmsucr  6503  ecovicom  6657  ecoviass  6659  ecovidi  6661  nnnninfeq  7140  nninfwlpoimlemg  7187  carden2bex  7202  addcompig  7342  addasspig  7343  mulcompig  7344  mulasspig  7345  distrpig  7346  addassnqg  7395  addnq0mo  7460  mulnq0mo  7461  nqnq0a  7467  nqnq0m  7468  distrnq0  7472  mulcomnq0  7473  addassnq0  7475  addcmpblnr  7752  mulcmpblnrlemg  7753  addsrmo  7756  mulsrmo  7757  ltsrprg  7760  recexgt0sr  7786  mulgt0sr  7791  mulextsr1lem  7793  addcnsrec  7855  mulcnsrec  7856  pitonnlem2  7860  recidpirqlemcalc  7870  axaddcom  7883  adddir  7962  mul32  8101  mul31  8102  add32  8130  add4  8132  sub32  8205  sub4  8216  subdir  8357  mulneg2  8367  mulreim  8575  apadd1  8579  apneg  8582  divassap  8661  divdirap  8668  divmul13ap  8686  divmul24ap  8687  divdiv32ap  8691  conjmulap  8700  zeo  9372  xaddcom  9875  xnegdi  9882  xaddass  9883  xaddass2  9884  xpncan  9885  xadd4d  9899  lincmb01cmp  10017  iccf1o  10018  flhalf  10316  modqvalp1  10357  modqdi  10406  modqsubdir  10407  frecuzrdgg  10430  seq3shft2  10487  seq3caopr3  10495  seq3caopr  10497  seq3f1olemqsumkj  10512  seq3f1olemqsumk  10513  seq3f1olemqsum  10514  seq3homo  10524  seqfeq3  10526  seq3distr  10527  expp1  10541  expnegap0  10542  expaddzaplem  10577  expaddzap  10578  expmulzap  10580  sqneg  10593  sqdivap  10598  subsq2  10642  binom2  10646  modqexp  10661  facp1  10724  bcm1k  10754  bcp1n  10755  bcval5  10757  omgadd  10796  hashun  10799  hashxp  10820  shftfibg  10843  shftfib  10846  shftval  10848  2shfti  10854  seq3shft  10861  crre  10880  remim  10883  mulreap  10887  reneg  10891  readd  10892  remullem  10894  redivap  10897  imneg  10899  imadd  10900  imdivap  10904  cjcj  10906  cjadd  10907  cjmulrcl  10910  cjneg  10913  imval2  10917  resqrexlemcalc1  11037  absneg  11073  sqabsadd  11078  sqabssub  11079  absmul  11092  absresq  11101  absexp  11102  absexpzap  11103  bdtrilem  11261  xrmaxiflemcom  11271  xrmaxadd  11283  xrminrecl  11295  xrminadd  11297  serf0  11374  summodclem3  11402  fsum3  11409  isumss  11413  fisumss  11414  fsumadd  11428  isummulc1  11449  isumdivapc  11450  fsum2dlemstep  11456  fisumcom2  11460  fisum0diag2  11469  fsummulc2  11470  fsummulc1  11471  fsumdivapc  11472  fsumconst  11476  telfsumo  11488  fsumparts  11492  binomlem  11505  isumshft  11512  arisum2  11521  geolim  11533  geo2sum  11536  geo2lim  11538  cvgratnnlemseq  11548  cvgratz  11554  mertenslem2  11558  prodfrecap  11568  prodfdivap  11569  prodmodclem2a  11598  fprodntrivap  11606  fprodssdc  11612  fprodmul  11613  fprodabs  11638  fprod2dlemstep  11644  fprodcom2fi  11648  fprodrec  11651  efcllemp  11680  efcj  11695  efexp  11704  resinval  11737  recosval  11738  cosneg  11749  efival  11754  sinadd  11758  cosadd  11759  addcos  11768  sin2t  11771  cos2t  11772  dvdsmodexp  11816  odd2np1lem  11891  oexpneg  11896  neggcd  11998  gcdabs2  12005  mulgcd  12031  mulgcdr  12033  gcddiv  12034  rplpwr  12042  eucalgval  12068  eucalginv  12070  eucalg  12073  neglcm  12089  lcmgcd  12092  mulgcddvds  12108  qredeu  12111  nn0gcdsq  12214  phimullem  12239  prmdiv  12249  coprimeprodsq  12271  pythagtriplem1  12279  pythagtriplem3  12281  pythagtriplem4  12282  pythagtriplem12  12289  pceulem  12308  pceu  12309  pcqmul  12317  pcexp  12323  pcneg  12338  pcadd  12353  pcmpt  12355  pcmpt2  12356  pcbc  12363  4sqlem7  12396  4sqlem10  12399  mul4sqlem  12405  ennnfonelemp1  12421  setsabsd  12515  setscom  12516  ressbasd  12541  strressid  12545  ressinbasd  12548  ressressg  12549  ressplusgd  12602  imasival  12745  qusin  12765  fvprif  12781  xpsfeq  12783  grpidpropdg  12812  mnd32g  12850  mnd4g  12852  0mhm  12895  mhmco  12896  grpinvcnv  12965  grpinvpropdg  12972  grpinvsub  12979  grpaddsubass  12987  grpsubpropdg  13001  grpsubpropd2  13002  imasgrp2  13005  imasgrp  13006  qusgrp2  13008  mulgnnp1  13023  mulgnegnn  13025  mulgaddcom  13039  mulginvcom  13040  mulgnndir  13044  mulgnn0ass  13051  mhmmulg  13056  mulgpropdg  13057  subginv  13073  subgsub  13078  subgmulg  13080  eqglact  13117  ablsub4  13150  ablsub32  13159  imasabl  13171  mgpress  13183  rngsubdi  13203  rngsubdir  13204  imasrng  13208  dfur2g  13214  srgass  13223  srgmulgass  13241  srgpcomp  13242  srglmhm  13245  srgrmhm  13246  crngcom  13266  ringass  13268  ringcom  13283  ringsubdi  13306  ringsubdir  13307  mulgass2  13308  imasring  13312  opprrng  13325  opprring  13327  oppr0g  13329  oppr1g  13330  opprnegg  13331  mulgass3  13333  dvdsrvald  13341  unitlinv  13374  unitrinv  13375  dvrfvald  13381  dvrass  13387  dvrdir  13391  rdivmuldivd  13392  rngidpropdg  13394  dvdsrpropdg  13395  unitpropdg  13396  invrpropdg  13397  subrguss  13456  subrginv  13457  subrgdv  13458  lmodcom  13522  lmodsubdir  13534  rmodislmod  13540  lsppropd  13621  srascag  13631  sravscag  13632  ixpsnbasval  13655  rsp0  13682  lidlrsppropdg  13684  rnglidlmsgrp  13686  zlmlemg  13786  zlmsca  13790  tgdom  13868  txbasval  14063  cnmpt11  14079  cnmpt21  14087  setsmsbasg  14275  bdbl  14299  dvmulxxbr  14462  dvimulf  14466  dvcj  14469  dvfre  14470  dvrecap  14473  dvef  14484  sinperlem  14525  coshalfpip  14539  ptolemy  14541  tangtx  14555  relogef  14581  rpcxpadd  14622  rpmulcxp  14626  rpdivcxp  14628  cxpmul  14629  abscxp  14631  rpcxpsqrt  14638  rpabscxpbnd  14655  rplogbreexp  14667  rprelogbmul  14669  rprelogbdiv  14671  lgsneg  14721  lgsmod  14723  lgsdir2  14730  lgsdirprm  14731  lgsdir  14732  lgsdi  14734  lgssq  14737  lgssq2  14738  lgsdirnn0  14744  lgsdinn0  14745  lgseisenlem1  14746  2sqlem3  14760  bj-charfundcALT  14857  nninfsellemeqinf  15062  refeq  15073