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  5572  fvco2  5582  resfunexg  5734  fcof1  5779  fliftfun  5792  caovdir2d  6046  caov32d  6050  caov31d  6052  caov4d  6054  caovlem2d  6062  caofcom  6101  cnvf1olem  6220  tfrlem1  6304  tfrlemisucaccv  6321  tfr1onlemsucaccv  6337  tfrcllemsucaccv  6350  frecrdg  6404  oav2  6459  omv2  6461  omsuc  6468  nnmsucr  6484  ecovicom  6638  ecoviass  6640  ecovidi  6642  nnnninfeq  7121  nninfwlpoimlemg  7168  carden2bex  7183  addcompig  7323  addasspig  7324  mulcompig  7325  mulasspig  7326  distrpig  7327  addassnqg  7376  addnq0mo  7441  mulnq0mo  7442  nqnq0a  7448  nqnq0m  7449  distrnq0  7453  mulcomnq0  7454  addassnq0  7456  addcmpblnr  7733  mulcmpblnrlemg  7734  addsrmo  7737  mulsrmo  7738  ltsrprg  7741  recexgt0sr  7767  mulgt0sr  7772  mulextsr1lem  7774  addcnsrec  7836  mulcnsrec  7837  pitonnlem2  7841  recidpirqlemcalc  7851  axaddcom  7864  adddir  7943  mul32  8081  mul31  8082  add32  8110  add4  8112  sub32  8185  sub4  8196  subdir  8337  mulneg2  8347  mulreim  8555  apadd1  8559  apneg  8562  divassap  8641  divdirap  8648  divmul13ap  8666  divmul24ap  8667  divdiv32ap  8671  conjmulap  8680  zeo  9352  xaddcom  9855  xnegdi  9862  xaddass  9863  xaddass2  9864  xpncan  9865  xadd4d  9879  lincmb01cmp  9997  iccf1o  9998  flhalf  10295  modqvalp1  10336  modqdi  10385  modqsubdir  10386  frecuzrdgg  10409  seq3shft2  10466  seq3caopr3  10474  seq3caopr  10476  seq3f1olemqsumkj  10491  seq3f1olemqsumk  10492  seq3f1olemqsum  10493  seq3homo  10503  seqfeq3  10505  seq3distr  10506  expp1  10520  expnegap0  10521  expaddzaplem  10556  expaddzap  10557  expmulzap  10559  sqneg  10572  sqdivap  10577  subsq2  10620  binom2  10624  modqexp  10639  facp1  10701  bcm1k  10731  bcp1n  10732  bcval5  10734  omgadd  10773  hashun  10776  hashxp  10797  shftfibg  10820  shftfib  10823  shftval  10825  2shfti  10831  seq3shft  10838  crre  10857  remim  10860  mulreap  10864  reneg  10868  readd  10869  remullem  10871  redivap  10874  imneg  10876  imadd  10877  imdivap  10881  cjcj  10883  cjadd  10884  cjmulrcl  10887  cjneg  10890  imval2  10894  resqrexlemcalc1  11014  absneg  11050  sqabsadd  11055  sqabssub  11056  absmul  11069  absresq  11078  absexp  11079  absexpzap  11080  bdtrilem  11238  xrmaxiflemcom  11248  xrmaxadd  11260  xrminrecl  11272  xrminadd  11274  serf0  11351  summodclem3  11379  fsum3  11386  isumss  11390  fisumss  11391  fsumadd  11405  isummulc1  11426  isumdivapc  11427  fsum2dlemstep  11433  fisumcom2  11437  fisum0diag2  11446  fsummulc2  11447  fsummulc1  11448  fsumdivapc  11449  fsumconst  11453  telfsumo  11465  fsumparts  11469  binomlem  11482  isumshft  11489  arisum2  11498  geolim  11510  geo2sum  11513  geo2lim  11515  cvgratnnlemseq  11525  cvgratz  11531  mertenslem2  11535  prodfrecap  11545  prodfdivap  11546  prodmodclem2a  11575  fprodntrivap  11583  fprodssdc  11589  fprodmul  11590  fprodabs  11615  fprod2dlemstep  11621  fprodcom2fi  11625  fprodrec  11628  efcllemp  11657  efcj  11672  efexp  11681  resinval  11714  recosval  11715  cosneg  11726  efival  11731  sinadd  11735  cosadd  11736  addcos  11745  sin2t  11748  cos2t  11749  dvdsmodexp  11793  odd2np1lem  11867  oexpneg  11872  neggcd  11974  gcdabs2  11981  mulgcd  12007  mulgcdr  12009  gcddiv  12010  rplpwr  12018  eucalgval  12044  eucalginv  12046  eucalg  12049  neglcm  12065  lcmgcd  12068  mulgcddvds  12084  qredeu  12087  nn0gcdsq  12190  phimullem  12215  prmdiv  12225  coprimeprodsq  12247  pythagtriplem1  12255  pythagtriplem3  12257  pythagtriplem4  12258  pythagtriplem12  12265  pceulem  12284  pceu  12285  pcqmul  12293  pcexp  12299  pcneg  12314  pcadd  12329  pcmpt  12331  pcmpt2  12332  pcbc  12339  4sqlem7  12372  4sqlem10  12375  mul4sqlem  12381  ennnfonelemp1  12397  setsabsd  12491  setscom  12492  ressbasd  12517  strressid  12520  ressinbasd  12523  ressressg  12524  ressplusgd  12577  grpidpropdg  12723  mnd32g  12758  mnd4g  12760  0mhm  12801  mhmco  12802  grpinvcnv  12866  grpinvpropdg  12873  grpinvsub  12880  grpaddsubass  12888  grpsubpropdg  12902  grpsubpropd2  12903  mulgnnp1  12919  mulgnegnn  12921  mulgaddcom  12934  mulginvcom  12935  mulgnndir  12939  mulgnn0ass  12946  mhmmulg  12951  mulgpropdg  12952  subginv  12967  subgsub  12972  subgmulg  12974  ablsub4  13016  ablsub32  13025  mgpress  13041  dfur2g  13045  srgass  13054  srgmulgass  13072  srgpcomp  13073  srglmhm  13076  srgrmhm  13077  crngcom  13097  ringass  13099  ringcom  13114  ringsubdi  13133  rngsubdir  13134  mulgass2  13135  opprring  13148  oppr0g  13150  oppr1g  13151  opprnegg  13152  mulgass3  13153  dvdsrvald  13161  unitlinv  13194  unitrinv  13195  dvrfvald  13201  dvrass  13207  dvrdir  13211  rdivmuldivd  13212  rngidpropdg  13214  dvdsrpropdg  13215  unitpropdg  13216  invrpropdg  13217  tgdom  13354  txbasval  13549  cnmpt11  13565  cnmpt21  13573  setsmsbasg  13761  bdbl  13785  dvmulxxbr  13948  dvimulf  13952  dvcj  13955  dvfre  13956  dvrecap  13959  dvef  13970  sinperlem  14011  coshalfpip  14025  ptolemy  14027  tangtx  14041  relogef  14067  rpcxpadd  14108  rpmulcxp  14112  rpdivcxp  14114  cxpmul  14115  abscxp  14117  rpcxpsqrt  14124  rpabscxpbnd  14141  rplogbreexp  14153  rprelogbmul  14155  rprelogbdiv  14157  lgsneg  14207  lgsmod  14209  lgsdir2  14216  lgsdirprm  14217  lgsdir  14218  lgsdi  14220  lgssq  14223  lgssq2  14224  lgsdirnn0  14230  lgsdinn0  14231  2sqlem3  14235  bj-charfundcALT  14332  nninfsellemeqinf  14536  refeq  14547