Theorem 3eqtr4d 2183

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

Syntax hints:   -> wi 4   = wceq 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133

This theorem is referenced by:  fnsnfv  5488  fvco2  5498  resfunexg  5649  fcof1  5692  fliftfun  5705  caovdir2d  5955  caov32d  5959  caov31d  5961  caov4d  5963  caovlem2d  5971  caofcom  6013  cnvf1olem  6129  tfrlem1  6213  tfrlemisucaccv  6230  tfr1onlemsucaccv  6246  tfrcllemsucaccv  6259  frecrdg  6313  oav2  6367  omv2  6369  omsuc  6376  nnmsucr  6392  ecovicom  6545  ecoviass  6547  ecovidi  6549  carden2bex  7062  addcompig  7161  addasspig  7162  mulcompig  7163  mulasspig  7164  distrpig  7165  addassnqg  7214  addnq0mo  7279  mulnq0mo  7280  nqnq0a  7286  nqnq0m  7287  distrnq0  7291  mulcomnq0  7292  addassnq0  7294  addcmpblnr  7571  mulcmpblnrlemg  7572  addsrmo  7575  mulsrmo  7576  ltsrprg  7579  recexgt0sr  7605  mulgt0sr  7610  mulextsr1lem  7612  addcnsrec  7674  mulcnsrec  7675  pitonnlem2  7679  recidpirqlemcalc  7689  axaddcom  7702  adddir  7781  mul32  7916  mul31  7917  add32  7945  add4  7947  sub32  8020  sub4  8031  subdir  8172  mulneg2  8182  mulreim  8390  apadd1  8394  apneg  8397  divassap  8474  divdirap  8481  divmul13ap  8499  divmul24ap  8500  divdiv32ap  8504  conjmulap  8513  zeo  9180  xaddcom  9674  xnegdi  9681  xaddass  9682  xaddass2  9683  xpncan  9684  xadd4d  9698  lincmb01cmp  9816  iccf1o  9817  flhalf  10106  modqvalp1  10147  modqdi  10196  modqsubdir  10197  frecuzrdgg  10220  seq3shft2  10277  seq3caopr3  10285  seq3caopr  10287  seq3f1olemqsumkj  10302  seq3f1olemqsumk  10303  seq3f1olemqsum  10304  seq3homo  10314  seqfeq3  10316  seq3distr  10317  expp1  10331  expnegap0  10332  expaddzaplem  10367  expaddzap  10368  expmulzap  10370  sqneg  10383  sqdivap  10388  subsq2  10431  binom2  10434  facp1  10508  bcm1k  10538  bcp1n  10539  bcval5  10541  omgadd  10580  hashun  10583  hashxp  10604  shftfibg  10624  shftfib  10627  shftval  10629  2shfti  10635  seq3shft  10642  crre  10661  remim  10664  mulreap  10668  reneg  10672  readd  10673  remullem  10675  redivap  10678  imneg  10680  imadd  10681  imdivap  10685  cjcj  10687  cjadd  10688  cjmulrcl  10691  cjneg  10694  imval2  10698  resqrexlemcalc1  10818  absneg  10854  sqabsadd  10859  sqabssub  10860  absmul  10873  absresq  10882  absexp  10883  absexpzap  10884  bdtrilem  11042  xrmaxiflemcom  11050  xrmaxadd  11062  xrminrecl  11074  xrminadd  11076  serf0  11153  summodclem3  11181  fsum3  11188  isumss  11192  fisumss  11193  fsumadd  11207  isummulc1  11228  isumdivapc  11229  fsum2dlemstep  11235  fisumcom2  11239  fisum0diag2  11248  fsummulc2  11249  fsummulc1  11250  fsumdivapc  11251  fsumconst  11255  telfsumo  11267  fsumparts  11271  binomlem  11284  isumshft  11291  arisum2  11300  geolim  11312  geo2sum  11315  geo2lim  11317  cvgratnnlemseq  11327  cvgratz  11333  mertenslem2  11337  prodfrecap  11347  prodfdivap  11348  prodmodclem2a  11377  efcllemp  11401  efcj  11416  efexp  11425  resinval  11458  recosval  11459  cosneg  11470  efival  11475  sinadd  11479  cosadd  11480  addcos  11489  sin2t  11492  cos2t  11493  odd2np1lem  11605  oexpneg  11610  neggcd  11707  gcdabs2  11714  mulgcd  11740  mulgcdr  11742  gcddiv  11743  rplpwr  11751  eucalgval  11771  eucalginv  11773  eucalg  11776  neglcm  11792  lcmgcd  11795  mulgcddvds  11811  qredeu  11814  nn0gcdsq  11914  phimullem  11937  ennnfonelemp1  11955  setsabsd  12037  setscom  12038  tgdom  12280  txbasval  12475  cnmpt11  12491  cnmpt21  12499  setsmsbasg  12687  bdbl  12711  dvmulxxbr  12874  dvimulf  12878  dvcj  12881  dvfre  12882  dvrecap  12885  dvef  12896  sinperlem  12937  coshalfpip  12951  ptolemy  12953  tangtx  12967  relogef  12993  rpcxpadd  13034  rpmulcxp  13038  rpdivcxp  13040  cxpmul  13041  abscxp  13043  rpcxpsqrt  13050  rpabscxpbnd  13067  rplogbreexp  13078  rprelogbmul  13080  rprelogbdiv  13082  nninfalllemn  13377  nninfsellemeqinf  13387  refeq  13398