Theorem 3eqtr4d 2274

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

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

This theorem is referenced by:  fnsnfv  5714  fvco2  5724  resfunexg  5883  fcof1  5934  fliftfun  5947  caovdir2d  6209  caov32d  6213  caov31d  6215  caov4d  6217  caovlem2d  6225  caofcom  6275  caofdig  6278  cnvf1olem  6398  tfrlem1  6517  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  frecrdg  6617  oav2  6674  omv2  6676  omsuc  6683  nnmsucr  6699  ecovicom  6855  ecoviass  6857  ecovidi  6859  nnnninfeq  7387  nninfwlpoimlemg  7434  carden2bex  7454  addcompig  7609  addasspig  7610  mulcompig  7611  mulasspig  7612  distrpig  7613  addassnqg  7662  addnq0mo  7727  mulnq0mo  7728  nqnq0a  7734  nqnq0m  7735  distrnq0  7739  mulcomnq0  7740  addassnq0  7742  addcmpblnr  8019  mulcmpblnrlemg  8020  addsrmo  8023  mulsrmo  8024  ltsrprg  8027  recexgt0sr  8053  mulgt0sr  8058  mulextsr1lem  8060  addcnsrec  8122  mulcnsrec  8123  pitonnlem2  8127  recidpirqlemcalc  8137  axaddcom  8150  adddir  8230  mul32  8368  mul31  8369  add32  8397  add4  8399  sub32  8472  sub4  8483  subdir  8624  mulneg2  8634  mulreim  8843  apadd1  8847  apneg  8850  divassap  8929  divdirap  8936  divmul13ap  8954  divmul24ap  8955  divdiv32ap  8959  conjmulap  8968  zeo  9646  xaddcom  10157  xnegdi  10164  xaddass  10165  xaddass2  10166  xpncan  10167  xadd4d  10181  lincmb01cmp  10299  iccf1o  10301  flhalf  10625  modqvalp1  10668  modqdi  10717  modqsubdir  10718  frecuzrdgg  10741  seq3shft2  10806  seqshft2g  10807  seq3caopr3  10816  seqcaopr3g  10817  seq3caopr  10820  seqcaoprg  10821  seq3f1olemqsumkj  10836  seq3f1olemqsumk  10837  seq3f1olemqsum  10838  seqf1oglem2a  10843  seqf1oglem2  10845  seqf1og  10846  seq3homo  10852  seqfeq3  10854  seqhomog  10855  seqfeq4g  10856  seq3distr  10857  expp1  10871  expnegap0  10872  expaddzaplem  10907  expaddzap  10908  expmulzap  10910  sqneg  10923  sqdivap  10928  subsq2  10972  binom2  10976  modqexp  10991  facp1  11055  bcm1k  11085  bcp1n  11086  bcval5  11088  omgadd  11128  hashun  11131  hashxp  11153  csbwrdg  11209  ccatass  11251  lswccatn0lsw  11254  swrdlsw  11316  swrdswrd  11352  wrd2ind  11370  swrdccatin1  11372  swrdccatin2  11376  pfxccatin12lem2  11378  pfxccatin12lem3  11379  pfxccatpfx1  11383  swrdccat3blem  11386  cats1catd  11415  shftfibg  11460  shftfib  11463  shftval  11465  2shfti  11471  seq3shft  11478  crre  11497  remim  11500  mulreap  11504  reneg  11508  readd  11509  remullem  11511  redivap  11514  imneg  11516  imadd  11517  imdivap  11521  cjcj  11523  cjadd  11524  cjmulrcl  11527  cjneg  11530  imval2  11534  resqrexlemcalc1  11654  absneg  11690  sqabsadd  11695  sqabssub  11696  absmul  11709  absresq  11718  absexp  11719  absexpzap  11720  bdtrilem  11879  xrmaxiflemcom  11889  xrmaxadd  11901  xrminrecl  11913  xrminadd  11915  serf0  11992  summodclem3  12021  fsum3  12028  isumss  12032  fisumss  12033  fsumadd  12047  isummulc1  12068  isumdivapc  12069  fsum2dlemstep  12075  fisumcom2  12079  fisum0diag2  12088  fsummulc2  12089  fsummulc1  12090  fsumdivapc  12091  fsumconst  12095  telfsumo  12107  fsumparts  12111  binomlem  12124  isumshft  12131  arisum2  12140  geolim  12152  geo2sum  12155  geo2lim  12157  cvgratnnlemseq  12167  cvgratz  12173  mertenslem2  12177  prodfrecap  12187  prodfdivap  12188  prodmodclem2a  12217  fprodntrivap  12225  fprodssdc  12231  fprodmul  12232  fprodabs  12257  fprod2dlemstep  12263  fprodcom2fi  12267  fprodrec  12270  efcllemp  12299  efcj  12314  efexp  12323  resinval  12356  recosval  12357  cosneg  12368  efival  12373  sinadd  12377  cosadd  12378  addcos  12387  sin2t  12390  cos2t  12391  dvdsmodexp  12436  odd2np1lem  12513  oexpneg  12518  neggcd  12634  gcdabs2  12641  mulgcd  12667  mulgcdr  12669  gcddiv  12670  rplpwr  12678  eucalgval  12706  eucalginv  12708  eucalg  12711  neglcm  12727  lcmgcd  12730  mulgcddvds  12746  qredeu  12749  nn0gcdsq  12852  phimullem  12877  prmdiv  12887  coprimeprodsq  12910  pythagtriplem1  12918  pythagtriplem3  12920  pythagtriplem4  12921  pythagtriplem12  12928  pceulem  12947  pceu  12948  pcqmul  12956  pcexp  12962  pcneg  12978  pcadd  12993  pcmpt  12996  pcmpt2  12997  pcbc  13004  4sqlem7  13037  4sqlem10  13040  mul4sqlem  13046  4sqlem11  13054  ennnfonelemp1  13107  setsabsd  13201  setscom  13202  ressbasd  13230  strressid  13234  ressinbasd  13237  ressressg  13238  ressplusgd  13292  prdsval  13436  pwsplusgval  13458  pwsmulrval  13459  imasival  13469  qusin  13489  fvprif  13506  xpsfeq  13508  grpidpropdg  13537  gsumpropd  13555  gsumpropd2  13556  gsumress  13558  prdssgrpd  13578  mnd32g  13590  mnd4g  13592  prdsidlem  13610  prdsmndd  13611  pws0g  13614  imasmnd2  13615  0mhm  13649  resmhm  13650  mhmco  13653  gsumwmhm  13661  grpinvcnv  13731  grpinvpropdg  13738  grpinvsub  13745  grpaddsubass  13753  grpsubpropdg  13767  grpsubpropd2  13768  prdsinvlem  13771  pwsinvg  13775  pwssub  13776  imasgrp2  13777  imasgrp  13778  qusgrp2  13780  mulgnnp1  13797  mulgnegnn  13799  mulgaddcom  13813  mulginvcom  13814  mulgnndir  13818  mulgnn0ass  13825  mhmmulg  13830  mulgpropdg  13831  submmulg  13833  subginv  13848  subgsub  13853  subgmulg  13855  eqglact  13892  ghmsub  13918  ghmmulg  13923  resghm  13927  ghmeql  13934  conjghm  13943  ablsub4  13980  ablsub32  13989  imasabl  14003  gsumfzreidx  14004  gsumfzmptfidmadd  14006  gsumfzconst  14008  mgpress  14025  rngsubdi  14045  rngsubdir  14046  imasrng  14050  dfur2g  14056  srgass  14065  srgmulgass  14083  srgpcomp  14084  srglmhm  14087  srgrmhm  14088  crngcom  14108  ringass  14110  ringcom  14125  ringsubdi  14150  ringsubdir  14151  mulgass2  14152  ringlghm  14155  ringrghm  14156  imasring  14158  opprrng  14171  opprring  14173  oppr0g  14175  oppr1g  14176  opprnegg  14177  mulgass3  14179  dvdsrvald  14188  unitlinv  14221  unitrinv  14222  dvrfvald  14228  dvrass  14234  dvrdir  14238  rdivmuldivd  14239  rngidpropdg  14241  dvdsrpropdg  14242  unitpropdg  14243  invrpropdg  14244  rhm1  14262  rhmopp  14271  subrguss  14331  subrginv  14332  subrgdv  14333  rrgsupp  14361  lmodcom  14429  lmodsubdir  14441  rmodislmod  14447  lsppropd  14528  srascag  14538  sravscag  14539  ixpsnbasval  14562  rsp0  14589  lidlrsppropdg  14591  rnglidlmsgrp  14593  gsumfzfsumlemm  14683  expghmap  14703  mulgghm2  14704  mulgrhm  14705  zlmlemg  14724  zlmsca  14728  znle  14733  psrbasg  14775  psrplusgg  14779  psrlinv  14785  tgdom  14883  txbasval  15078  cnmpt11  15094  cnmpt21  15102  setsmsbasg  15290  bdbl  15314  dvmulxxbr  15513  dvimulf  15517  dvcj  15520  dvfre  15521  dvrecap  15524  dvmptc  15528  dvmptfsum  15536  dvef  15538  plyaddlem1  15558  plyrecj  15574  dvply1  15576  sinperlem  15619  coshalfpip  15633  ptolemy  15635  tangtx  15649  relogef  15675  rpcxpadd  15716  rpmulcxp  15720  rpdivcxp  15722  cxpmul  15723  rpcxpmul2  15724  abscxp  15726  rpcxpsqrt  15733  rpabscxpbnd  15751  rplogbreexp  15764  rprelogbmul  15766  rprelogbdiv  15768  pellexlem3  15793  1sgmprm  15808  perfect1  15812  perfectlem2  15814  perfect  15815  lgsneg  15843  lgsmod  15845  lgsdir2  15852  lgsdirprm  15853  lgsdir  15854  lgsdi  15856  lgssq  15859  lgssq2  15860  lgsdirnn0  15866  lgsdinn0  15867  gausslemma2dlem6  15886  lgseisenlem1  15889  lgseisenlem3  15891  lgseisenlem4  15892  lgsquadlem1  15896  lgsquad2  15902  2sqlem3  15936  setsiedg  15993  vtxdeqd  16237  vtxdfifiun  16238  trlsegvdegfi  16408  depindlem3  16449  bj-charfundcALT  16525  nninfsellemeqinf  16742  refeq  16756  gfsumval  16809  gsumgfsumlem  16812