Theorem 3eqtr4d 2208

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

Syntax hints:   -> wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  fnsnfv  5544  fvco2  5554  resfunexg  5705  fcof1  5750  fliftfun  5763  caovdir2d  6014  caov32d  6018  caov31d  6020  caov4d  6022  caovlem2d  6030  caofcom  6072  cnvf1olem  6188  tfrlem1  6272  tfrlemisucaccv  6289  tfr1onlemsucaccv  6305  tfrcllemsucaccv  6318  frecrdg  6372  oav2  6427  omv2  6429  omsuc  6436  nnmsucr  6452  ecovicom  6605  ecoviass  6607  ecovidi  6609  nnnninfeq  7088  carden2bex  7141  addcompig  7266  addasspig  7267  mulcompig  7268  mulasspig  7269  distrpig  7270  addassnqg  7319  addnq0mo  7384  mulnq0mo  7385  nqnq0a  7391  nqnq0m  7392  distrnq0  7396  mulcomnq0  7397  addassnq0  7399  addcmpblnr  7676  mulcmpblnrlemg  7677  addsrmo  7680  mulsrmo  7681  ltsrprg  7684  recexgt0sr  7710  mulgt0sr  7715  mulextsr1lem  7717  addcnsrec  7779  mulcnsrec  7780  pitonnlem2  7784  recidpirqlemcalc  7794  axaddcom  7807  adddir  7886  mul32  8024  mul31  8025  add32  8053  add4  8055  sub32  8128  sub4  8139  subdir  8280  mulneg2  8290  mulreim  8498  apadd1  8502  apneg  8505  divassap  8582  divdirap  8589  divmul13ap  8607  divmul24ap  8608  divdiv32ap  8612  conjmulap  8621  zeo  9292  xaddcom  9793  xnegdi  9800  xaddass  9801  xaddass2  9802  xpncan  9803  xadd4d  9817  lincmb01cmp  9935  iccf1o  9936  flhalf  10233  modqvalp1  10274  modqdi  10323  modqsubdir  10324  frecuzrdgg  10347  seq3shft2  10404  seq3caopr3  10412  seq3caopr  10414  seq3f1olemqsumkj  10429  seq3f1olemqsumk  10430  seq3f1olemqsum  10431  seq3homo  10441  seqfeq3  10443  seq3distr  10444  expp1  10458  expnegap0  10459  expaddzaplem  10494  expaddzap  10495  expmulzap  10497  sqneg  10510  sqdivap  10515  subsq2  10558  binom2  10562  modqexp  10577  facp1  10639  bcm1k  10669  bcp1n  10670  bcval5  10672  omgadd  10711  hashun  10714  hashxp  10735  shftfibg  10758  shftfib  10761  shftval  10763  2shfti  10769  seq3shft  10776  crre  10795  remim  10798  mulreap  10802  reneg  10806  readd  10807  remullem  10809  redivap  10812  imneg  10814  imadd  10815  imdivap  10819  cjcj  10821  cjadd  10822  cjmulrcl  10825  cjneg  10828  imval2  10832  resqrexlemcalc1  10952  absneg  10988  sqabsadd  10993  sqabssub  10994  absmul  11007  absresq  11016  absexp  11017  absexpzap  11018  bdtrilem  11176  xrmaxiflemcom  11186  xrmaxadd  11198  xrminrecl  11210  xrminadd  11212  serf0  11289  summodclem3  11317  fsum3  11324  isumss  11328  fisumss  11329  fsumadd  11343  isummulc1  11364  isumdivapc  11365  fsum2dlemstep  11371  fisumcom2  11375  fisum0diag2  11384  fsummulc2  11385  fsummulc1  11386  fsumdivapc  11387  fsumconst  11391  telfsumo  11403  fsumparts  11407  binomlem  11420  isumshft  11427  arisum2  11436  geolim  11448  geo2sum  11451  geo2lim  11453  cvgratnnlemseq  11463  cvgratz  11469  mertenslem2  11473  prodfrecap  11483  prodfdivap  11484  prodmodclem2a  11513  fprodntrivap  11521  fprodssdc  11527  fprodmul  11528  fprodabs  11553  fprod2dlemstep  11559  fprodcom2fi  11563  fprodrec  11566  efcllemp  11595  efcj  11610  efexp  11619  resinval  11652  recosval  11653  cosneg  11664  efival  11669  sinadd  11673  cosadd  11674  addcos  11683  sin2t  11686  cos2t  11687  dvdsmodexp  11731  odd2np1lem  11805  oexpneg  11810  neggcd  11912  gcdabs2  11919  mulgcd  11945  mulgcdr  11947  gcddiv  11948  rplpwr  11956  eucalgval  11982  eucalginv  11984  eucalg  11987  neglcm  12003  lcmgcd  12006  mulgcddvds  12022  qredeu  12025  nn0gcdsq  12128  phimullem  12153  prmdiv  12163  coprimeprodsq  12185  pythagtriplem1  12193  pythagtriplem3  12195  pythagtriplem4  12196  pythagtriplem12  12203  pceulem  12222  pceu  12223  pcqmul  12231  pcexp  12237  pcneg  12252  pcadd  12267  pcmpt  12269  pcmpt2  12270  pcbc  12277  4sqlem7  12310  4sqlem10  12313  mul4sqlem  12319  ennnfonelemp1  12335  setsabsd  12429  setscom  12430  tgdom  12672  txbasval  12867  cnmpt11  12883  cnmpt21  12891  setsmsbasg  13079  bdbl  13103  dvmulxxbr  13266  dvimulf  13270  dvcj  13273  dvfre  13274  dvrecap  13277  dvef  13288  sinperlem  13329  coshalfpip  13343  ptolemy  13345  tangtx  13359  relogef  13385  rpcxpadd  13426  rpmulcxp  13430  rpdivcxp  13432  cxpmul  13433  abscxp  13435  rpcxpsqrt  13442  rpabscxpbnd  13459  rplogbreexp  13471  rprelogbmul  13473  rprelogbdiv  13475  lgsneg  13525  lgsmod  13527  lgsdir2  13534  lgsdirprm  13535  lgsdir  13536  lgsdi  13538  lgssq  13541  lgssq2  13542  lgsdirnn0  13548  lgsdinn0  13549  2sqlem3  13553  bj-charfundcALT  13651  nninfsellemeqinf  13856  refeq  13867