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  5575  fvco2  5585  resfunexg  5737  fcof1  5783  fliftfun  5796  caovdir2d  6050  caov32d  6054  caov31d  6056  caov4d  6058  caovlem2d  6066  caofcom  6105  cnvf1olem  6224  tfrlem1  6308  tfrlemisucaccv  6325  tfr1onlemsucaccv  6341  tfrcllemsucaccv  6354  frecrdg  6408  oav2  6463  omv2  6465  omsuc  6472  nnmsucr  6488  ecovicom  6642  ecoviass  6644  ecovidi  6646  nnnninfeq  7125  nninfwlpoimlemg  7172  carden2bex  7187  addcompig  7327  addasspig  7328  mulcompig  7329  mulasspig  7330  distrpig  7331  addassnqg  7380  addnq0mo  7445  mulnq0mo  7446  nqnq0a  7452  nqnq0m  7453  distrnq0  7457  mulcomnq0  7458  addassnq0  7460  addcmpblnr  7737  mulcmpblnrlemg  7738  addsrmo  7741  mulsrmo  7742  ltsrprg  7745  recexgt0sr  7771  mulgt0sr  7776  mulextsr1lem  7778  addcnsrec  7840  mulcnsrec  7841  pitonnlem2  7845  recidpirqlemcalc  7855  axaddcom  7868  adddir  7947  mul32  8086  mul31  8087  add32  8115  add4  8117  sub32  8190  sub4  8201  subdir  8342  mulneg2  8352  mulreim  8560  apadd1  8564  apneg  8567  divassap  8646  divdirap  8653  divmul13ap  8671  divmul24ap  8672  divdiv32ap  8676  conjmulap  8685  zeo  9357  xaddcom  9860  xnegdi  9867  xaddass  9868  xaddass2  9869  xpncan  9870  xadd4d  9884  lincmb01cmp  10002  iccf1o  10003  flhalf  10301  modqvalp1  10342  modqdi  10391  modqsubdir  10392  frecuzrdgg  10415  seq3shft2  10472  seq3caopr3  10480  seq3caopr  10482  seq3f1olemqsumkj  10497  seq3f1olemqsumk  10498  seq3f1olemqsum  10499  seq3homo  10509  seqfeq3  10511  seq3distr  10512  expp1  10526  expnegap0  10527  expaddzaplem  10562  expaddzap  10563  expmulzap  10565  sqneg  10578  sqdivap  10583  subsq2  10627  binom2  10631  modqexp  10646  facp1  10709  bcm1k  10739  bcp1n  10740  bcval5  10742  omgadd  10781  hashun  10784  hashxp  10805  shftfibg  10828  shftfib  10831  shftval  10833  2shfti  10839  seq3shft  10846  crre  10865  remim  10868  mulreap  10872  reneg  10876  readd  10877  remullem  10879  redivap  10882  imneg  10884  imadd  10885  imdivap  10889  cjcj  10891  cjadd  10892  cjmulrcl  10895  cjneg  10898  imval2  10902  resqrexlemcalc1  11022  absneg  11058  sqabsadd  11063  sqabssub  11064  absmul  11077  absresq  11086  absexp  11087  absexpzap  11088  bdtrilem  11246  xrmaxiflemcom  11256  xrmaxadd  11268  xrminrecl  11280  xrminadd  11282  serf0  11359  summodclem3  11387  fsum3  11394  isumss  11398  fisumss  11399  fsumadd  11413  isummulc1  11434  isumdivapc  11435  fsum2dlemstep  11441  fisumcom2  11445  fisum0diag2  11454  fsummulc2  11455  fsummulc1  11456  fsumdivapc  11457  fsumconst  11461  telfsumo  11473  fsumparts  11477  binomlem  11490  isumshft  11497  arisum2  11506  geolim  11518  geo2sum  11521  geo2lim  11523  cvgratnnlemseq  11533  cvgratz  11539  mertenslem2  11543  prodfrecap  11553  prodfdivap  11554  prodmodclem2a  11583  fprodntrivap  11591  fprodssdc  11597  fprodmul  11598  fprodabs  11623  fprod2dlemstep  11629  fprodcom2fi  11633  fprodrec  11636  efcllemp  11665  efcj  11680  efexp  11689  resinval  11722  recosval  11723  cosneg  11734  efival  11739  sinadd  11743  cosadd  11744  addcos  11753  sin2t  11756  cos2t  11757  dvdsmodexp  11801  odd2np1lem  11876  oexpneg  11881  neggcd  11983  gcdabs2  11990  mulgcd  12016  mulgcdr  12018  gcddiv  12019  rplpwr  12027  eucalgval  12053  eucalginv  12055  eucalg  12058  neglcm  12074  lcmgcd  12077  mulgcddvds  12093  qredeu  12096  nn0gcdsq  12199  phimullem  12224  prmdiv  12234  coprimeprodsq  12256  pythagtriplem1  12264  pythagtriplem3  12266  pythagtriplem4  12267  pythagtriplem12  12274  pceulem  12293  pceu  12294  pcqmul  12302  pcexp  12308  pcneg  12323  pcadd  12338  pcmpt  12340  pcmpt2  12341  pcbc  12348  4sqlem7  12381  4sqlem10  12384  mul4sqlem  12390  ennnfonelemp1  12406  setsabsd  12500  setscom  12501  ressbasd  12526  strressid  12529  ressinbasd  12532  ressressg  12533  ressplusgd  12586  imasival  12726  qusin  12745  fvprif  12761  xpsfeq  12763  grpidpropdg  12792  mnd32g  12827  mnd4g  12829  0mhm  12872  mhmco  12873  grpinvcnv  12937  grpinvpropdg  12944  grpinvsub  12951  grpaddsubass  12959  grpsubpropdg  12973  grpsubpropd2  12974  mulgnnp1  12990  mulgnegnn  12992  mulgaddcom  13005  mulginvcom  13006  mulgnndir  13010  mulgnn0ass  13017  mhmmulg  13022  mulgpropdg  13023  subginv  13039  subgsub  13044  subgmulg  13046  eqglact  13082  ablsub4  13114  ablsub32  13123  mgpress  13139  dfur2g  13143  srgass  13152  srgmulgass  13170  srgpcomp  13171  srglmhm  13174  srgrmhm  13175  crngcom  13195  ringass  13197  ringcom  13212  ringsubdi  13231  rngsubdir  13232  mulgass2  13233  opprring  13247  oppr0g  13249  oppr1g  13250  opprnegg  13251  mulgass3  13252  dvdsrvald  13260  unitlinv  13293  unitrinv  13294  dvrfvald  13300  dvrass  13306  dvrdir  13310  rdivmuldivd  13311  rngidpropdg  13313  dvdsrpropdg  13314  unitpropdg  13315  invrpropdg  13316  subrguss  13355  subrginv  13356  subrgdv  13357  tgdom  13542  txbasval  13737  cnmpt11  13753  cnmpt21  13761  setsmsbasg  13949  bdbl  13973  dvmulxxbr  14136  dvimulf  14140  dvcj  14143  dvfre  14144  dvrecap  14147  dvef  14158  sinperlem  14199  coshalfpip  14213  ptolemy  14215  tangtx  14229  relogef  14255  rpcxpadd  14296  rpmulcxp  14300  rpdivcxp  14302  cxpmul  14303  abscxp  14305  rpcxpsqrt  14312  rpabscxpbnd  14329  rplogbreexp  14341  rprelogbmul  14343  rprelogbdiv  14345  lgsneg  14395  lgsmod  14397  lgsdir2  14404  lgsdirprm  14405  lgsdir  14406  lgsdi  14408  lgssq  14411  lgssq2  14412  lgsdirnn0  14418  lgsdinn0  14419  lgseisenlem1  14420  2sqlem3  14434  bj-charfundcALT  14531  nninfsellemeqinf  14735  refeq  14746