Theorem 3eqtr4d 2239

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 2232	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
5	1, 4	eqtr4d 2232	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  fnsnfv  5623  fvco2  5633  resfunexg  5786  fcof1  5833  fliftfun  5846  caovdir2d  6104  caov32d  6108  caov31d  6110  caov4d  6112  caovlem2d  6120  caofcom  6170  caofdig  6173  cnvf1olem  6291  tfrlem1  6375  tfrlemisucaccv  6392  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  frecrdg  6475  oav2  6530  omv2  6532  omsuc  6539  nnmsucr  6555  ecovicom  6711  ecoviass  6713  ecovidi  6715  nnnninfeq  7203  nninfwlpoimlemg  7250  carden2bex  7268  addcompig  7413  addasspig  7414  mulcompig  7415  mulasspig  7416  distrpig  7417  addassnqg  7466  addnq0mo  7531  mulnq0mo  7532  nqnq0a  7538  nqnq0m  7539  distrnq0  7543  mulcomnq0  7544  addassnq0  7546  addcmpblnr  7823  mulcmpblnrlemg  7824  addsrmo  7827  mulsrmo  7828  ltsrprg  7831  recexgt0sr  7857  mulgt0sr  7862  mulextsr1lem  7864  addcnsrec  7926  mulcnsrec  7927  pitonnlem2  7931  recidpirqlemcalc  7941  axaddcom  7954  adddir  8034  mul32  8173  mul31  8174  add32  8202  add4  8204  sub32  8277  sub4  8288  subdir  8429  mulneg2  8439  mulreim  8648  apadd1  8652  apneg  8655  divassap  8734  divdirap  8741  divmul13ap  8759  divmul24ap  8760  divdiv32ap  8764  conjmulap  8773  zeo  9448  xaddcom  9953  xnegdi  9960  xaddass  9961  xaddass2  9962  xpncan  9963  xadd4d  9977  lincmb01cmp  10095  iccf1o  10096  flhalf  10409  modqvalp1  10452  modqdi  10501  modqsubdir  10502  frecuzrdgg  10525  seq3shft2  10590  seqshft2g  10591  seq3caopr3  10600  seqcaopr3g  10601  seq3caopr  10604  seqcaoprg  10605  seq3f1olemqsumkj  10620  seq3f1olemqsumk  10621  seq3f1olemqsum  10622  seqf1oglem2a  10627  seqf1oglem2  10629  seqf1og  10630  seq3homo  10636  seqfeq3  10638  seqhomog  10639  seqfeq4g  10640  seq3distr  10641  expp1  10655  expnegap0  10656  expaddzaplem  10691  expaddzap  10692  expmulzap  10694  sqneg  10707  sqdivap  10712  subsq2  10756  binom2  10760  modqexp  10775  facp1  10839  bcm1k  10869  bcp1n  10870  bcval5  10872  omgadd  10911  hashun  10914  hashxp  10935  csbwrdg  10981  shftfibg  11002  shftfib  11005  shftval  11007  2shfti  11013  seq3shft  11020  crre  11039  remim  11042  mulreap  11046  reneg  11050  readd  11051  remullem  11053  redivap  11056  imneg  11058  imadd  11059  imdivap  11063  cjcj  11065  cjadd  11066  cjmulrcl  11069  cjneg  11072  imval2  11076  resqrexlemcalc1  11196  absneg  11232  sqabsadd  11237  sqabssub  11238  absmul  11251  absresq  11260  absexp  11261  absexpzap  11262  bdtrilem  11421  xrmaxiflemcom  11431  xrmaxadd  11443  xrminrecl  11455  xrminadd  11457  serf0  11534  summodclem3  11562  fsum3  11569  isumss  11573  fisumss  11574  fsumadd  11588  isummulc1  11609  isumdivapc  11610  fsum2dlemstep  11616  fisumcom2  11620  fisum0diag2  11629  fsummulc2  11630  fsummulc1  11631  fsumdivapc  11632  fsumconst  11636  telfsumo  11648  fsumparts  11652  binomlem  11665  isumshft  11672  arisum2  11681  geolim  11693  geo2sum  11696  geo2lim  11698  cvgratnnlemseq  11708  cvgratz  11714  mertenslem2  11718  prodfrecap  11728  prodfdivap  11729  prodmodclem2a  11758  fprodntrivap  11766  fprodssdc  11772  fprodmul  11773  fprodabs  11798  fprod2dlemstep  11804  fprodcom2fi  11808  fprodrec  11811  efcllemp  11840  efcj  11855  efexp  11864  resinval  11897  recosval  11898  cosneg  11909  efival  11914  sinadd  11918  cosadd  11919  addcos  11928  sin2t  11931  cos2t  11932  dvdsmodexp  11977  odd2np1lem  12054  oexpneg  12059  neggcd  12175  gcdabs2  12182  mulgcd  12208  mulgcdr  12210  gcddiv  12211  rplpwr  12219  eucalgval  12247  eucalginv  12249  eucalg  12252  neglcm  12268  lcmgcd  12271  mulgcddvds  12287  qredeu  12290  nn0gcdsq  12393  phimullem  12418  prmdiv  12428  coprimeprodsq  12451  pythagtriplem1  12459  pythagtriplem3  12461  pythagtriplem4  12462  pythagtriplem12  12469  pceulem  12488  pceu  12489  pcqmul  12497  pcexp  12503  pcneg  12519  pcadd  12534  pcmpt  12537  pcmpt2  12538  pcbc  12545  4sqlem7  12578  4sqlem10  12581  mul4sqlem  12587  4sqlem11  12595  ennnfonelemp1  12648  setsabsd  12742  setscom  12743  ressbasd  12770  strressid  12774  ressinbasd  12777  ressressg  12778  ressplusgd  12831  prdsval  12975  pwsplusgval  12997  pwsmulrval  12998  imasival  13008  qusin  13028  fvprif  13045  xpsfeq  13047  grpidpropdg  13076  gsumpropd  13094  gsumpropd2  13095  gsumress  13097  prdssgrpd  13117  mnd32g  13129  mnd4g  13131  prdsidlem  13149  prdsmndd  13150  pws0g  13153  imasmnd2  13154  0mhm  13188  resmhm  13189  mhmco  13192  gsumwmhm  13200  grpinvcnv  13270  grpinvpropdg  13277  grpinvsub  13284  grpaddsubass  13292  grpsubpropdg  13306  grpsubpropd2  13307  prdsinvlem  13310  pwsinvg  13314  pwssub  13315  imasgrp2  13316  imasgrp  13317  qusgrp2  13319  mulgnnp1  13336  mulgnegnn  13338  mulgaddcom  13352  mulginvcom  13353  mulgnndir  13357  mulgnn0ass  13364  mhmmulg  13369  mulgpropdg  13370  submmulg  13372  subginv  13387  subgsub  13392  subgmulg  13394  eqglact  13431  ghmsub  13457  ghmmulg  13462  resghm  13466  ghmeql  13473  conjghm  13482  ablsub4  13519  ablsub32  13528  imasabl  13542  gsumfzreidx  13543  gsumfzmptfidmadd  13545  gsumfzconst  13547  mgpress  13563  rngsubdi  13583  rngsubdir  13584  imasrng  13588  dfur2g  13594  srgass  13603  srgmulgass  13621  srgpcomp  13622  srglmhm  13625  srgrmhm  13626  crngcom  13646  ringass  13648  ringcom  13663  ringsubdi  13688  ringsubdir  13689  mulgass2  13690  ringlghm  13693  ringrghm  13694  imasring  13696  opprrng  13709  opprring  13711  oppr0g  13713  oppr1g  13714  opprnegg  13715  mulgass3  13717  dvdsrvald  13725  unitlinv  13758  unitrinv  13759  dvrfvald  13765  dvrass  13771  dvrdir  13775  rdivmuldivd  13776  rngidpropdg  13778  dvdsrpropdg  13779  unitpropdg  13780  invrpropdg  13781  rhm1  13799  rhmopp  13808  subrguss  13868  subrginv  13869  subrgdv  13870  lmodcom  13965  lmodsubdir  13977  rmodislmod  13983  lsppropd  14064  srascag  14074  sravscag  14075  ixpsnbasval  14098  rsp0  14125  lidlrsppropdg  14127  rnglidlmsgrp  14129  gsumfzfsumlemm  14219  expghmap  14239  mulgghm2  14240  mulgrhm  14241  zlmlemg  14260  zlmsca  14264  znle  14269  psrbasg  14303  psrplusgg  14306  psrlinv  14312  tgdom  14392  txbasval  14587  cnmpt11  14603  cnmpt21  14611  setsmsbasg  14799  bdbl  14823  dvmulxxbr  15022  dvimulf  15026  dvcj  15029  dvfre  15030  dvrecap  15033  dvmptc  15037  dvmptfsum  15045  dvef  15047  plyaddlem1  15067  plyrecj  15083  dvply1  15085  sinperlem  15128  coshalfpip  15142  ptolemy  15144  tangtx  15158  relogef  15184  rpcxpadd  15225  rpmulcxp  15229  rpdivcxp  15231  cxpmul  15232  rpcxpmul2  15233  abscxp  15235  rpcxpsqrt  15242  rpabscxpbnd  15260  rplogbreexp  15273  rprelogbmul  15275  rprelogbdiv  15277  1sgmprm  15314  perfect1  15318  perfectlem2  15320  perfect  15321  lgsneg  15349  lgsmod  15351  lgsdir2  15358  lgsdirprm  15359  lgsdir  15360  lgsdi  15362  lgssq  15365  lgssq2  15366  lgsdirnn0  15372  lgsdinn0  15373  gausslemma2dlem6  15392  lgseisenlem1  15395  lgseisenlem3  15397  lgseisenlem4  15398  lgsquadlem1  15402  lgsquad2  15408  2sqlem3  15442  bj-charfundcALT  15539  nninfsellemeqinf  15747  refeq  15759