Theorem 3eqtr4d 2275

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  fnsnfv  5736  fvco2  5746  resfunexg  5905  fcof1  5956  fliftfun  5969  caovdir2d  6231  caov32d  6235  caov31d  6237  caov4d  6239  caovlem2d  6247  caofcom  6297  caofdig  6300  cnvf1olem  6420  tfrlem1  6539  tfrlemisucaccv  6556  tfr1onlemsucaccv  6572  tfrcllemsucaccv  6585  frecrdg  6639  oav2  6696  omv2  6698  omsuc  6705  nnmsucr  6721  ecovicom  6877  ecoviass  6879  ecovidi  6881  nnnninfeq  7419  nninfwlpoimlemg  7466  carden2bex  7486  addcompig  7644  addasspig  7645  mulcompig  7646  mulasspig  7647  distrpig  7648  addassnqg  7697  addnq0mo  7762  mulnq0mo  7763  nqnq0a  7769  nqnq0m  7770  distrnq0  7774  mulcomnq0  7775  addassnq0  7777  addcmpblnr  8054  mulcmpblnrlemg  8055  addsrmo  8058  mulsrmo  8059  ltsrprg  8062  recexgt0sr  8088  mulgt0sr  8093  mulextsr1lem  8095  addcnsrec  8157  mulcnsrec  8158  pitonnlem2  8162  recidpirqlemcalc  8172  axaddcom  8185  adddir  8265  mul32  8403  mul31  8404  add32  8432  add4  8434  sub32  8507  sub4  8518  subdir  8659  mulneg2  8669  mulreim  8878  apadd1  8882  apneg  8885  divassap  8964  divdirap  8971  divmul13ap  8989  divmul24ap  8990  divdiv32ap  8994  conjmulap  9003  zeo  9683  xaddcom  10194  xnegdi  10201  xaddass  10202  xaddass2  10203  xpncan  10204  xadd4d  10218  lincmb01cmp  10336  iccf1o  10338  flhalf  10662  modqvalp1  10705  modqdi  10754  modqsubdir  10755  frecuzrdgg  10778  seq3shft2  10843  seqshft2g  10844  seq3caopr3  10853  seqcaopr3g  10854  seq3caopr  10857  seqcaoprg  10858  seq3f1olemqsumkj  10873  seq3f1olemqsumk  10874  seq3f1olemqsum  10875  seqf1oglem2a  10880  seqf1oglem2  10882  seqf1og  10883  seq3homo  10889  seqfeq3  10891  seqhomog  10892  seqfeq4g  10893  seq3distr  10894  expp1  10908  expnegap0  10909  expaddzaplem  10944  expaddzap  10945  expmulzap  10947  sqneg  10960  sqdivap  10965  subsq2  11009  binom2  11013  modqexp  11028  facp1  11092  bcm1k  11122  bcp1n  11123  bcval5  11125  omgadd  11166  hashun  11169  hashxp  11191  hashfibclem  11206  csbwrdg  11254  ccatass  11296  lswccatn0lsw  11299  swrdlsw  11361  swrdswrd  11397  wrd2ind  11415  swrdccatin1  11417  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccatin12lem3  11424  pfxccatpfx1  11428  swrdccat3blem  11431  cats1catd  11460  shftfibg  11505  shftfib  11508  shftval  11510  2shfti  11516  seq3shft  11523  crre  11542  remim  11545  mulreap  11549  reneg  11553  readd  11554  remullem  11556  redivap  11559  imneg  11561  imadd  11562  imdivap  11566  cjcj  11568  cjadd  11569  cjmulrcl  11572  cjneg  11575  imval2  11579  resqrexlemcalc1  11699  absneg  11735  sqabsadd  11740  sqabssub  11741  absmul  11754  absresq  11763  absexp  11764  absexpzap  11765  bdtrilem  11924  xrmaxiflemcom  11934  xrmaxadd  11946  xrminrecl  11958  xrminadd  11960  serf0  12037  summodclem3  12066  fsum3  12073  isumss  12077  fisumss  12078  fsumadd  12092  isummulc1  12113  isumdivapc  12114  fsum2dlemstep  12120  fisumcom2  12124  fisum0diag2  12133  fsummulc2  12134  fsummulc1  12135  fsumdivapc  12136  fsumconst  12140  telfsumo  12152  fsumparts  12156  binomlem  12169  isumshft  12176  arisum2  12185  geolim  12197  geo2sum  12200  geo2lim  12202  cvgratnnlemseq  12212  cvgratz  12218  mertenslem2  12222  prodfrecap  12232  prodfdivap  12233  prodmodclem2a  12262  fprodntrivap  12270  fprodssdc  12276  fprodmul  12277  fprodabs  12302  fprod2dlemstep  12308  fprodcom2fi  12312  fprodrec  12315  efcllemp  12344  efcj  12359  efexp  12368  resinval  12401  recosval  12402  cosneg  12413  efival  12418  sinadd  12422  cosadd  12423  addcos  12432  sin2t  12435  cos2t  12436  dvdsmodexp  12481  odd2np1lem  12558  oexpneg  12563  neggcd  12679  gcdabs2  12686  mulgcd  12712  mulgcdr  12714  gcddiv  12715  rplpwr  12723  eucalgval  12751  eucalginv  12753  eucalg  12756  neglcm  12772  lcmgcd  12775  mulgcddvds  12791  qredeu  12794  nn0gcdsq  12897  phimullem  12922  prmdiv  12932  coprimeprodsq  12955  pythagtriplem1  12963  pythagtriplem3  12965  pythagtriplem4  12966  pythagtriplem12  12973  pceulem  12992  pceu  12993  pcqmul  13001  pcexp  13007  pcneg  13023  pcadd  13038  pcmpt  13041  pcmpt2  13042  pcbc  13049  4sqlem7  13082  4sqlem10  13085  mul4sqlem  13091  4sqlem11  13099  ennnfonelemp1  13157  setsabsd  13251  setscom  13252  ressbasd  13280  strressid  13284  ressinbasd  13287  ressressg  13288  ressplusgd  13342  prdsval  13486  pwsplusgval  13508  pwsmulrval  13509  imasival  13519  qusin  13539  fvprif  13556  xpsfeq  13558  grpidpropdg  13587  gsumpropd  13605  gsumpropd2  13606  gsumress  13608  prdssgrpd  13628  mnd32g  13640  mnd4g  13642  prdsidlem  13660  prdsmndd  13661  pws0g  13664  imasmnd2  13665  0mhm  13699  resmhm  13700  mhmco  13703  gsumwmhm  13711  grpinvcnv  13781  grpinvpropdg  13788  grpinvsub  13795  grpaddsubass  13803  grpsubpropdg  13817  grpsubpropd2  13818  prdsinvlem  13821  pwsinvg  13825  pwssub  13826  imasgrp2  13827  imasgrp  13828  qusgrp2  13830  mulgnnp1  13847  mulgnegnn  13849  mulgaddcom  13863  mulginvcom  13864  mulgnndir  13868  mulgnn0ass  13875  mhmmulg  13880  mulgpropdg  13881  submmulg  13883  subginv  13898  subgsub  13903  subgmulg  13905  eqglact  13942  ghmsub  13968  ghmmulg  13973  resghm  13977  ghmeql  13984  conjghm  13993  ablsub4  14030  ablsub32  14039  imasabl  14053  gsumfzreidx  14054  gsumfzmptfidmadd  14056  gsumfzconst  14058  mgpress  14075  rngsubdi  14095  rngsubdir  14096  imasrng  14100  dfur2g  14106  srgass  14115  srgmulgass  14133  srgpcomp  14134  srglmhm  14137  srgrmhm  14138  crngcom  14158  ringass  14160  ringcom  14175  ringsubdi  14200  ringsubdir  14201  mulgass2  14202  ringlghm  14205  ringrghm  14206  imasring  14208  opprrng  14221  opprring  14223  oppr0g  14225  oppr1g  14226  opprnegg  14227  mulgass3  14229  dvdsrvald  14238  unitlinv  14271  unitrinv  14272  dvrfvald  14278  dvrass  14284  dvrdir  14288  rdivmuldivd  14289  rngidpropdg  14291  dvdsrpropdg  14292  unitpropdg  14293  invrpropdg  14294  rhm1  14312  rhmopp  14321  subrguss  14381  subrginv  14382  subrgdv  14383  rrgsupp  14411  lmodcom  14481  lmodsubdir  14493  rmodislmod  14499  lsppropd  14580  srascag  14590  sravscag  14591  ixpsnbasval  14614  rsp0  14641  lidlrsppropdg  14643  rnglidlmsgrp  14645  gsumfzfsumlemm  14735  expghmap  14755  mulgghm2  14756  mulgrhm  14757  zlmlemg  14776  zlmsca  14780  znle  14785  psrbasg  14829  psrplusgg  14833  psrlinv  14839  tgdom  14937  txbasval  15132  cnmpt11  15148  cnmpt21  15156  setsmsbasg  15344  bdbl  15368  dvmulxxbr  15567  dvimulf  15571  dvcj  15574  dvfre  15575  dvrecap  15578  dvmptc  15582  dvmptfsum  15590  dvef  15592  plyaddlem1  15612  plyrecj  15628  dvply1  15630  sinperlem  15673  coshalfpip  15687  ptolemy  15689  tangtx  15703  relogef  15729  rpcxpadd  15770  rpmulcxp  15774  rpdivcxp  15776  cxpmul  15777  rpcxpmul2  15778  abscxp  15780  rpcxpsqrt  15787  rpabscxpbnd  15805  rplogbreexp  15818  rprelogbmul  15820  rprelogbdiv  15822  pellexlem3  15847  1sgmprm  15862  perfect1  15866  perfectlem2  15868  perfect  15869  lgsneg  15897  lgsmod  15899  lgsdir2  15906  lgsdirprm  15907  lgsdir  15908  lgsdi  15910  lgssq  15913  lgssq2  15914  lgsdirnn0  15920  lgsdinn0  15921  gausslemma2dlem6  15940  lgseisenlem1  15943  lgseisenlem3  15945  lgseisenlem4  15946  lgsquadlem1  15950  lgsquad2  15956  2sqlem3  15990  setsiedg  16047  vtxdeqd  16291  vtxdfifiun  16292  trlsegvdegfi  16462  depindlem3  16503  bj-charfundcALT  16579  nninfsellemeqinf  16794  refeq  16808  gfsumval  16862  gsumgfsumlem  16865