Theorem 3eqtr4d 2272

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  fnsnfv  5695  fvco2  5705  resfunexg  5864  fcof1  5913  fliftfun  5926  caovdir2d  6188  caov32d  6192  caov31d  6194  caov4d  6196  caovlem2d  6204  caofcom  6255  caofdig  6258  cnvf1olem  6376  tfrlem1  6460  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  frecrdg  6560  oav2  6617  omv2  6619  omsuc  6626  nnmsucr  6642  ecovicom  6798  ecoviass  6800  ecovidi  6802  nnnninfeq  7306  nninfwlpoimlemg  7353  carden2bex  7373  addcompig  7527  addasspig  7528  mulcompig  7529  mulasspig  7530  distrpig  7531  addassnqg  7580  addnq0mo  7645  mulnq0mo  7646  nqnq0a  7652  nqnq0m  7653  distrnq0  7657  mulcomnq0  7658  addassnq0  7660  addcmpblnr  7937  mulcmpblnrlemg  7938  addsrmo  7941  mulsrmo  7942  ltsrprg  7945  recexgt0sr  7971  mulgt0sr  7976  mulextsr1lem  7978  addcnsrec  8040  mulcnsrec  8041  pitonnlem2  8045  recidpirqlemcalc  8055  axaddcom  8068  adddir  8148  mul32  8287  mul31  8288  add32  8316  add4  8318  sub32  8391  sub4  8402  subdir  8543  mulneg2  8553  mulreim  8762  apadd1  8766  apneg  8769  divassap  8848  divdirap  8855  divmul13ap  8873  divmul24ap  8874  divdiv32ap  8878  conjmulap  8887  zeo  9563  xaddcom  10069  xnegdi  10076  xaddass  10077  xaddass2  10078  xpncan  10079  xadd4d  10093  lincmb01cmp  10211  iccf1o  10212  flhalf  10534  modqvalp1  10577  modqdi  10626  modqsubdir  10627  frecuzrdgg  10650  seq3shft2  10715  seqshft2g  10716  seq3caopr3  10725  seqcaopr3g  10726  seq3caopr  10729  seqcaoprg  10730  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seqf1oglem2a  10752  seqf1oglem2  10754  seqf1og  10755  seq3homo  10761  seqfeq3  10763  seqhomog  10764  seqfeq4g  10765  seq3distr  10766  expp1  10780  expnegap0  10781  expaddzaplem  10816  expaddzap  10817  expmulzap  10819  sqneg  10832  sqdivap  10837  subsq2  10881  binom2  10885  modqexp  10900  facp1  10964  bcm1k  10994  bcp1n  10995  bcval5  10997  omgadd  11036  hashun  11039  hashxp  11061  csbwrdg  11114  ccatass  11156  lswccatn0lsw  11159  swrdlsw  11217  swrdswrd  11253  wrd2ind  11271  swrdccatin1  11273  swrdccatin2  11277  pfxccatin12lem2  11279  pfxccatin12lem3  11280  pfxccatpfx1  11284  swrdccat3blem  11287  cats1catd  11316  shftfibg  11347  shftfib  11350  shftval  11352  2shfti  11358  seq3shft  11365  crre  11384  remim  11387  mulreap  11391  reneg  11395  readd  11396  remullem  11398  redivap  11401  imneg  11403  imadd  11404  imdivap  11408  cjcj  11410  cjadd  11411  cjmulrcl  11414  cjneg  11417  imval2  11421  resqrexlemcalc1  11541  absneg  11577  sqabsadd  11582  sqabssub  11583  absmul  11596  absresq  11605  absexp  11606  absexpzap  11607  bdtrilem  11766  xrmaxiflemcom  11776  xrmaxadd  11788  xrminrecl  11800  xrminadd  11802  serf0  11879  summodclem3  11907  fsum3  11914  isumss  11918  fisumss  11919  fsumadd  11933  isummulc1  11954  isumdivapc  11955  fsum2dlemstep  11961  fisumcom2  11965  fisum0diag2  11974  fsummulc2  11975  fsummulc1  11976  fsumdivapc  11977  fsumconst  11981  telfsumo  11993  fsumparts  11997  binomlem  12010  isumshft  12017  arisum2  12026  geolim  12038  geo2sum  12041  geo2lim  12043  cvgratnnlemseq  12053  cvgratz  12059  mertenslem2  12063  prodfrecap  12073  prodfdivap  12074  prodmodclem2a  12103  fprodntrivap  12111  fprodssdc  12117  fprodmul  12118  fprodabs  12143  fprod2dlemstep  12149  fprodcom2fi  12153  fprodrec  12156  efcllemp  12185  efcj  12200  efexp  12209  resinval  12242  recosval  12243  cosneg  12254  efival  12259  sinadd  12263  cosadd  12264  addcos  12273  sin2t  12276  cos2t  12277  dvdsmodexp  12322  odd2np1lem  12399  oexpneg  12404  neggcd  12520  gcdabs2  12527  mulgcd  12553  mulgcdr  12555  gcddiv  12556  rplpwr  12564  eucalgval  12592  eucalginv  12594  eucalg  12597  neglcm  12613  lcmgcd  12616  mulgcddvds  12632  qredeu  12635  nn0gcdsq  12738  phimullem  12763  prmdiv  12773  coprimeprodsq  12796  pythagtriplem1  12804  pythagtriplem3  12806  pythagtriplem4  12807  pythagtriplem12  12814  pceulem  12833  pceu  12834  pcqmul  12842  pcexp  12848  pcneg  12864  pcadd  12879  pcmpt  12882  pcmpt2  12883  pcbc  12890  4sqlem7  12923  4sqlem10  12926  mul4sqlem  12932  4sqlem11  12940  ennnfonelemp1  12993  setsabsd  13087  setscom  13088  ressbasd  13116  strressid  13120  ressinbasd  13123  ressressg  13124  ressplusgd  13178  prdsval  13322  pwsplusgval  13344  pwsmulrval  13345  imasival  13355  qusin  13375  fvprif  13392  xpsfeq  13394  grpidpropdg  13423  gsumpropd  13441  gsumpropd2  13442  gsumress  13444  prdssgrpd  13464  mnd32g  13476  mnd4g  13478  prdsidlem  13496  prdsmndd  13497  pws0g  13500  imasmnd2  13501  0mhm  13535  resmhm  13536  mhmco  13539  gsumwmhm  13547  grpinvcnv  13617  grpinvpropdg  13624  grpinvsub  13631  grpaddsubass  13639  grpsubpropdg  13653  grpsubpropd2  13654  prdsinvlem  13657  pwsinvg  13661  pwssub  13662  imasgrp2  13663  imasgrp  13664  qusgrp2  13666  mulgnnp1  13683  mulgnegnn  13685  mulgaddcom  13699  mulginvcom  13700  mulgnndir  13704  mulgnn0ass  13711  mhmmulg  13716  mulgpropdg  13717  submmulg  13719  subginv  13734  subgsub  13739  subgmulg  13741  eqglact  13778  ghmsub  13804  ghmmulg  13809  resghm  13813  ghmeql  13820  conjghm  13829  ablsub4  13866  ablsub32  13875  imasabl  13889  gsumfzreidx  13890  gsumfzmptfidmadd  13892  gsumfzconst  13894  mgpress  13910  rngsubdi  13930  rngsubdir  13931  imasrng  13935  dfur2g  13941  srgass  13950  srgmulgass  13968  srgpcomp  13969  srglmhm  13972  srgrmhm  13973  crngcom  13993  ringass  13995  ringcom  14010  ringsubdi  14035  ringsubdir  14036  mulgass2  14037  ringlghm  14040  ringrghm  14041  imasring  14043  opprrng  14056  opprring  14058  oppr0g  14060  oppr1g  14061  opprnegg  14062  mulgass3  14064  dvdsrvald  14073  unitlinv  14106  unitrinv  14107  dvrfvald  14113  dvrass  14119  dvrdir  14123  rdivmuldivd  14124  rngidpropdg  14126  dvdsrpropdg  14127  unitpropdg  14128  invrpropdg  14129  rhm1  14147  rhmopp  14156  subrguss  14216  subrginv  14217  subrgdv  14218  lmodcom  14313  lmodsubdir  14325  rmodislmod  14331  lsppropd  14412  srascag  14422  sravscag  14423  ixpsnbasval  14446  rsp0  14473  lidlrsppropdg  14475  rnglidlmsgrp  14477  gsumfzfsumlemm  14567  expghmap  14587  mulgghm2  14588  mulgrhm  14589  zlmlemg  14608  zlmsca  14612  znle  14617  psrbasg  14654  psrplusgg  14658  psrlinv  14664  tgdom  14762  txbasval  14957  cnmpt11  14973  cnmpt21  14981  setsmsbasg  15169  bdbl  15193  dvmulxxbr  15392  dvimulf  15396  dvcj  15399  dvfre  15400  dvrecap  15403  dvmptc  15407  dvmptfsum  15415  dvef  15417  plyaddlem1  15437  plyrecj  15453  dvply1  15455  sinperlem  15498  coshalfpip  15512  ptolemy  15514  tangtx  15528  relogef  15554  rpcxpadd  15595  rpmulcxp  15599  rpdivcxp  15601  cxpmul  15602  rpcxpmul2  15603  abscxp  15605  rpcxpsqrt  15612  rpabscxpbnd  15630  rplogbreexp  15643  rprelogbmul  15645  rprelogbdiv  15647  1sgmprm  15684  perfect1  15688  perfectlem2  15690  perfect  15691  lgsneg  15719  lgsmod  15721  lgsdir2  15728  lgsdirprm  15729  lgsdir  15730  lgsdi  15732  lgssq  15735  lgssq2  15736  lgsdirnn0  15742  lgsdinn0  15743  gausslemma2dlem6  15762  lgseisenlem1  15765  lgseisenlem3  15767  lgseisenlem4  15768  lgsquadlem1  15772  lgsquad2  15778  2sqlem3  15812  setsiedg  15869  vtxdeqd  16056  vtxdfifiun  16057  bj-charfundcALT  16255  nninfsellemeqinf  16470  refeq  16484