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	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3eqtr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3eqtr4d	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr4d

Step	Hyp	Ref	Expression
1		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
2		3eqtr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
3		3eqtr4d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr4d 2267	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
5	1, 4	eqtr4d 2267	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  fnsnfv  5705  fvco2  5715  resfunexg  5874  fcof1  5923  fliftfun  5936  caovdir2d  6198  caov32d  6202  caov31d  6204  caov4d  6206  caovlem2d  6214  caofcom  6265  caofdig  6268  cnvf1olem  6388  tfrlem1  6473  tfrlemisucaccv  6490  tfr1onlemsucaccv  6506  tfrcllemsucaccv  6519  frecrdg  6573  oav2  6630  omv2  6632  omsuc  6639  nnmsucr  6655  ecovicom  6811  ecoviass  6813  ecovidi  6815  nnnninfeq  7326  nninfwlpoimlemg  7373  carden2bex  7393  addcompig  7548  addasspig  7549  mulcompig  7550  mulasspig  7551  distrpig  7552  addassnqg  7601  addnq0mo  7666  mulnq0mo  7667  nqnq0a  7673  nqnq0m  7674  distrnq0  7678  mulcomnq0  7679  addassnq0  7681  addcmpblnr  7958  mulcmpblnrlemg  7959  addsrmo  7962  mulsrmo  7963  ltsrprg  7966  recexgt0sr  7992  mulgt0sr  7997  mulextsr1lem  7999  addcnsrec  8061  mulcnsrec  8062  pitonnlem2  8066  recidpirqlemcalc  8076  axaddcom  8089  adddir  8169  mul32  8308  mul31  8309  add32  8337  add4  8339  sub32  8412  sub4  8423  subdir  8564  mulneg2  8574  mulreim  8783  apadd1  8787  apneg  8790  divassap  8869  divdirap  8876  divmul13ap  8894  divmul24ap  8895  divdiv32ap  8899  conjmulap  8908  zeo  9584  xaddcom  10095  xnegdi  10102  xaddass  10103  xaddass2  10104  xpncan  10105  xadd4d  10119  lincmb01cmp  10237  iccf1o  10238  flhalf  10561  modqvalp1  10604  modqdi  10653  modqsubdir  10654  frecuzrdgg  10677  seq3shft2  10742  seqshft2g  10743  seq3caopr3  10752  seqcaopr3g  10753  seq3caopr  10756  seqcaoprg  10757  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seq3f1olemqsum  10774  seqf1oglem2a  10779  seqf1oglem2  10781  seqf1og  10782  seq3homo  10788  seqfeq3  10790  seqhomog  10791  seqfeq4g  10792  seq3distr  10793  expp1  10807  expnegap0  10808  expaddzaplem  10843  expaddzap  10844  expmulzap  10846  sqneg  10859  sqdivap  10864  subsq2  10908  binom2  10912  modqexp  10927  facp1  10991  bcm1k  11021  bcp1n  11022  bcval5  11024  omgadd  11064  hashun  11067  hashxp  11089  csbwrdg  11142  ccatass  11184  lswccatn0lsw  11187  swrdlsw  11249  swrdswrd  11285  wrd2ind  11303  swrdccatin1  11305  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12lem3  11312  pfxccatpfx1  11316  swrdccat3blem  11319  cats1catd  11348  shftfibg  11380  shftfib  11383  shftval  11385  2shfti  11391  seq3shft  11398  crre  11417  remim  11420  mulreap  11424  reneg  11428  readd  11429  remullem  11431  redivap  11434  imneg  11436  imadd  11437  imdivap  11441  cjcj  11443  cjadd  11444  cjmulrcl  11447  cjneg  11450  imval2  11454  resqrexlemcalc1  11574  absneg  11610  sqabsadd  11615  sqabssub  11616  absmul  11629  absresq  11638  absexp  11639  absexpzap  11640  bdtrilem  11799  xrmaxiflemcom  11809  xrmaxadd  11821  xrminrecl  11833  xrminadd  11835  serf0  11912  summodclem3  11940  fsum3  11947  isumss  11951  fisumss  11952  fsumadd  11966  isummulc1  11987  isumdivapc  11988  fsum2dlemstep  11994  fisumcom2  11998  fisum0diag2  12007  fsummulc2  12008  fsummulc1  12009  fsumdivapc  12010  fsumconst  12014  telfsumo  12026  fsumparts  12030  binomlem  12043  isumshft  12050  arisum2  12059  geolim  12071  geo2sum  12074  geo2lim  12076  cvgratnnlemseq  12086  cvgratz  12092  mertenslem2  12096  prodfrecap  12106  prodfdivap  12107  prodmodclem2a  12136  fprodntrivap  12144  fprodssdc  12150  fprodmul  12151  fprodabs  12176  fprod2dlemstep  12182  fprodcom2fi  12186  fprodrec  12189  efcllemp  12218  efcj  12233  efexp  12242  resinval  12275  recosval  12276  cosneg  12287  efival  12292  sinadd  12296  cosadd  12297  addcos  12306  sin2t  12309  cos2t  12310  dvdsmodexp  12355  odd2np1lem  12432  oexpneg  12437  neggcd  12553  gcdabs2  12560  mulgcd  12586  mulgcdr  12588  gcddiv  12589  rplpwr  12597  eucalgval  12625  eucalginv  12627  eucalg  12630  neglcm  12646  lcmgcd  12649  mulgcddvds  12665  qredeu  12668  nn0gcdsq  12771  phimullem  12796  prmdiv  12806  coprimeprodsq  12829  pythagtriplem1  12837  pythagtriplem3  12839  pythagtriplem4  12840  pythagtriplem12  12847  pceulem  12866  pceu  12867  pcqmul  12875  pcexp  12881  pcneg  12897  pcadd  12912  pcmpt  12915  pcmpt2  12916  pcbc  12923  4sqlem7  12956  4sqlem10  12959  mul4sqlem  12965  4sqlem11  12973  ennnfonelemp1  13026  setsabsd  13120  setscom  13121  ressbasd  13149  strressid  13153  ressinbasd  13156  ressressg  13157  ressplusgd  13211  prdsval  13355  pwsplusgval  13377  pwsmulrval  13378  imasival  13388  qusin  13408  fvprif  13425  xpsfeq  13427  grpidpropdg  13456  gsumpropd  13474  gsumpropd2  13475  gsumress  13477  prdssgrpd  13497  mnd32g  13509  mnd4g  13511  prdsidlem  13529  prdsmndd  13530  pws0g  13533  imasmnd2  13534  0mhm  13568  resmhm  13569  mhmco  13572  gsumwmhm  13580  grpinvcnv  13650  grpinvpropdg  13657  grpinvsub  13664  grpaddsubass  13672  grpsubpropdg  13686  grpsubpropd2  13687  prdsinvlem  13690  pwsinvg  13694  pwssub  13695  imasgrp2  13696  imasgrp  13697  qusgrp2  13699  mulgnnp1  13716  mulgnegnn  13718  mulgaddcom  13732  mulginvcom  13733  mulgnndir  13737  mulgnn0ass  13744  mhmmulg  13749  mulgpropdg  13750  submmulg  13752  subginv  13767  subgsub  13772  subgmulg  13774  eqglact  13811  ghmsub  13837  ghmmulg  13842  resghm  13846  ghmeql  13853  conjghm  13862  ablsub4  13899  ablsub32  13908  imasabl  13922  gsumfzreidx  13923  gsumfzmptfidmadd  13925  gsumfzconst  13927  mgpress  13943  rngsubdi  13963  rngsubdir  13964  imasrng  13968  dfur2g  13974  srgass  13983  srgmulgass  14001  srgpcomp  14002  srglmhm  14005  srgrmhm  14006  crngcom  14026  ringass  14028  ringcom  14043  ringsubdi  14068  ringsubdir  14069  mulgass2  14070  ringlghm  14073  ringrghm  14074  imasring  14076  opprrng  14089  opprring  14091  oppr0g  14093  oppr1g  14094  opprnegg  14095  mulgass3  14097  dvdsrvald  14106  unitlinv  14139  unitrinv  14140  dvrfvald  14146  dvrass  14152  dvrdir  14156  rdivmuldivd  14157  rngidpropdg  14159  dvdsrpropdg  14160  unitpropdg  14161  invrpropdg  14162  rhm1  14180  rhmopp  14189  subrguss  14249  subrginv  14250  subrgdv  14251  lmodcom  14346  lmodsubdir  14358  rmodislmod  14364  lsppropd  14445  srascag  14455  sravscag  14456  ixpsnbasval  14479  rsp0  14506  lidlrsppropdg  14508  rnglidlmsgrp  14510  gsumfzfsumlemm  14600  expghmap  14620  mulgghm2  14621  mulgrhm  14622  zlmlemg  14641  zlmsca  14645  znle  14650  psrbasg  14687  psrplusgg  14691  psrlinv  14697  tgdom  14795  txbasval  14990  cnmpt11  15006  cnmpt21  15014  setsmsbasg  15202  bdbl  15226  dvmulxxbr  15425  dvimulf  15429  dvcj  15432  dvfre  15433  dvrecap  15436  dvmptc  15440  dvmptfsum  15448  dvef  15450  plyaddlem1  15470  plyrecj  15486  dvply1  15488  sinperlem  15531  coshalfpip  15545  ptolemy  15547  tangtx  15561  relogef  15587  rpcxpadd  15628  rpmulcxp  15632  rpdivcxp  15634  cxpmul  15635  rpcxpmul2  15636  abscxp  15638  rpcxpsqrt  15645  rpabscxpbnd  15663  rplogbreexp  15676  rprelogbmul  15678  rprelogbdiv  15680  1sgmprm  15717  perfect1  15721  perfectlem2  15723  perfect  15724  lgsneg  15752  lgsmod  15754  lgsdir2  15761  lgsdirprm  15762  lgsdir  15763  lgsdi  15765  lgssq  15768  lgssq2  15769  lgsdirnn0  15775  lgsdinn0  15776  gausslemma2dlem6  15795  lgseisenlem1  15798  lgseisenlem3  15800  lgseisenlem4  15801  lgsquadlem1  15805  lgsquad2  15811  2sqlem3  15845  setsiedg  15902  vtxdeqd  16146  vtxdfifiun  16147  bj-charfundcALT  16404  nninfsellemeqinf  16618  refeq  16632  gfsumval  16680  gsumgfsumlem  16683