Theorem 3eqtr4d 2247

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

Syntax hints:   → wi 4   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  fnsnfv  5637  fvco2  5647  resfunexg  5804  fcof1  5851  fliftfun  5864  caovdir2d  6122  caov32d  6126  caov31d  6128  caov4d  6130  caovlem2d  6138  caofcom  6188  caofdig  6191  cnvf1olem  6309  tfrlem1  6393  tfrlemisucaccv  6410  tfr1onlemsucaccv  6426  tfrcllemsucaccv  6439  frecrdg  6493  oav2  6548  omv2  6550  omsuc  6557  nnmsucr  6573  ecovicom  6729  ecoviass  6731  ecovidi  6733  nnnninfeq  7229  nninfwlpoimlemg  7276  carden2bex  7296  addcompig  7441  addasspig  7442  mulcompig  7443  mulasspig  7444  distrpig  7445  addassnqg  7494  addnq0mo  7559  mulnq0mo  7560  nqnq0a  7566  nqnq0m  7567  distrnq0  7571  mulcomnq0  7572  addassnq0  7574  addcmpblnr  7851  mulcmpblnrlemg  7852  addsrmo  7855  mulsrmo  7856  ltsrprg  7859  recexgt0sr  7885  mulgt0sr  7890  mulextsr1lem  7892  addcnsrec  7954  mulcnsrec  7955  pitonnlem2  7959  recidpirqlemcalc  7969  axaddcom  7982  adddir  8062  mul32  8201  mul31  8202  add32  8230  add4  8232  sub32  8305  sub4  8316  subdir  8457  mulneg2  8467  mulreim  8676  apadd1  8680  apneg  8683  divassap  8762  divdirap  8769  divmul13ap  8787  divmul24ap  8788  divdiv32ap  8792  conjmulap  8801  zeo  9477  xaddcom  9982  xnegdi  9989  xaddass  9990  xaddass2  9991  xpncan  9992  xadd4d  10006  lincmb01cmp  10124  iccf1o  10125  flhalf  10443  modqvalp1  10486  modqdi  10535  modqsubdir  10536  frecuzrdgg  10559  seq3shft2  10624  seqshft2g  10625  seq3caopr3  10634  seqcaopr3g  10635  seq3caopr  10638  seqcaoprg  10639  seq3f1olemqsumkj  10654  seq3f1olemqsumk  10655  seq3f1olemqsum  10656  seqf1oglem2a  10661  seqf1oglem2  10663  seqf1og  10664  seq3homo  10670  seqfeq3  10672  seqhomog  10673  seqfeq4g  10674  seq3distr  10675  expp1  10689  expnegap0  10690  expaddzaplem  10725  expaddzap  10726  expmulzap  10728  sqneg  10741  sqdivap  10746  subsq2  10790  binom2  10794  modqexp  10809  facp1  10873  bcm1k  10903  bcp1n  10904  bcval5  10906  omgadd  10945  hashun  10948  hashxp  10969  csbwrdg  11021  ccatass  11062  lswccatn0lsw  11065  shftfibg  11102  shftfib  11105  shftval  11107  2shfti  11113  seq3shft  11120  crre  11139  remim  11142  mulreap  11146  reneg  11150  readd  11151  remullem  11153  redivap  11156  imneg  11158  imadd  11159  imdivap  11163  cjcj  11165  cjadd  11166  cjmulrcl  11169  cjneg  11172  imval2  11176  resqrexlemcalc1  11296  absneg  11332  sqabsadd  11337  sqabssub  11338  absmul  11351  absresq  11360  absexp  11361  absexpzap  11362  bdtrilem  11521  xrmaxiflemcom  11531  xrmaxadd  11543  xrminrecl  11555  xrminadd  11557  serf0  11634  summodclem3  11662  fsum3  11669  isumss  11673  fisumss  11674  fsumadd  11688  isummulc1  11709  isumdivapc  11710  fsum2dlemstep  11716  fisumcom2  11720  fisum0diag2  11729  fsummulc2  11730  fsummulc1  11731  fsumdivapc  11732  fsumconst  11736  telfsumo  11748  fsumparts  11752  binomlem  11765  isumshft  11772  arisum2  11781  geolim  11793  geo2sum  11796  geo2lim  11798  cvgratnnlemseq  11808  cvgratz  11814  mertenslem2  11818  prodfrecap  11828  prodfdivap  11829  prodmodclem2a  11858  fprodntrivap  11866  fprodssdc  11872  fprodmul  11873  fprodabs  11898  fprod2dlemstep  11904  fprodcom2fi  11908  fprodrec  11911  efcllemp  11940  efcj  11955  efexp  11964  resinval  11997  recosval  11998  cosneg  12009  efival  12014  sinadd  12018  cosadd  12019  addcos  12028  sin2t  12031  cos2t  12032  dvdsmodexp  12077  odd2np1lem  12154  oexpneg  12159  neggcd  12275  gcdabs2  12282  mulgcd  12308  mulgcdr  12310  gcddiv  12311  rplpwr  12319  eucalgval  12347  eucalginv  12349  eucalg  12352  neglcm  12368  lcmgcd  12371  mulgcddvds  12387  qredeu  12390  nn0gcdsq  12493  phimullem  12518  prmdiv  12528  coprimeprodsq  12551  pythagtriplem1  12559  pythagtriplem3  12561  pythagtriplem4  12562  pythagtriplem12  12569  pceulem  12588  pceu  12589  pcqmul  12597  pcexp  12603  pcneg  12619  pcadd  12634  pcmpt  12637  pcmpt2  12638  pcbc  12645  4sqlem7  12678  4sqlem10  12681  mul4sqlem  12687  4sqlem11  12695  ennnfonelemp1  12748  setsabsd  12842  setscom  12843  ressbasd  12870  strressid  12874  ressinbasd  12877  ressressg  12878  ressplusgd  12932  prdsval  13076  pwsplusgval  13098  pwsmulrval  13099  imasival  13109  qusin  13129  fvprif  13146  xpsfeq  13148  grpidpropdg  13177  gsumpropd  13195  gsumpropd2  13196  gsumress  13198  prdssgrpd  13218  mnd32g  13230  mnd4g  13232  prdsidlem  13250  prdsmndd  13251  pws0g  13254  imasmnd2  13255  0mhm  13289  resmhm  13290  mhmco  13293  gsumwmhm  13301  grpinvcnv  13371  grpinvpropdg  13378  grpinvsub  13385  grpaddsubass  13393  grpsubpropdg  13407  grpsubpropd2  13408  prdsinvlem  13411  pwsinvg  13415  pwssub  13416  imasgrp2  13417  imasgrp  13418  qusgrp2  13420  mulgnnp1  13437  mulgnegnn  13439  mulgaddcom  13453  mulginvcom  13454  mulgnndir  13458  mulgnn0ass  13465  mhmmulg  13470  mulgpropdg  13471  submmulg  13473  subginv  13488  subgsub  13493  subgmulg  13495  eqglact  13532  ghmsub  13558  ghmmulg  13563  resghm  13567  ghmeql  13574  conjghm  13583  ablsub4  13620  ablsub32  13629  imasabl  13643  gsumfzreidx  13644  gsumfzmptfidmadd  13646  gsumfzconst  13648  mgpress  13664  rngsubdi  13684  rngsubdir  13685  imasrng  13689  dfur2g  13695  srgass  13704  srgmulgass  13722  srgpcomp  13723  srglmhm  13726  srgrmhm  13727  crngcom  13747  ringass  13749  ringcom  13764  ringsubdi  13789  ringsubdir  13790  mulgass2  13791  ringlghm  13794  ringrghm  13795  imasring  13797  opprrng  13810  opprring  13812  oppr0g  13814  oppr1g  13815  opprnegg  13816  mulgass3  13818  dvdsrvald  13826  unitlinv  13859  unitrinv  13860  dvrfvald  13866  dvrass  13872  dvrdir  13876  rdivmuldivd  13877  rngidpropdg  13879  dvdsrpropdg  13880  unitpropdg  13881  invrpropdg  13882  rhm1  13900  rhmopp  13909  subrguss  13969  subrginv  13970  subrgdv  13971  lmodcom  14066  lmodsubdir  14078  rmodislmod  14084  lsppropd  14165  srascag  14175  sravscag  14176  ixpsnbasval  14199  rsp0  14226  lidlrsppropdg  14228  rnglidlmsgrp  14230  gsumfzfsumlemm  14320  expghmap  14340  mulgghm2  14341  mulgrhm  14342  zlmlemg  14361  zlmsca  14365  znle  14370  psrbasg  14407  psrplusgg  14411  psrlinv  14417  tgdom  14515  txbasval  14710  cnmpt11  14726  cnmpt21  14734  setsmsbasg  14922  bdbl  14946  dvmulxxbr  15145  dvimulf  15149  dvcj  15152  dvfre  15153  dvrecap  15156  dvmptc  15160  dvmptfsum  15168  dvef  15170  plyaddlem1  15190  plyrecj  15206  dvply1  15208  sinperlem  15251  coshalfpip  15265  ptolemy  15267  tangtx  15281  relogef  15307  rpcxpadd  15348  rpmulcxp  15352  rpdivcxp  15354  cxpmul  15355  rpcxpmul2  15356  abscxp  15358  rpcxpsqrt  15365  rpabscxpbnd  15383  rplogbreexp  15396  rprelogbmul  15398  rprelogbdiv  15400  1sgmprm  15437  perfect1  15441  perfectlem2  15443  perfect  15444  lgsneg  15472  lgsmod  15474  lgsdir2  15481  lgsdirprm  15482  lgsdir  15483  lgsdi  15485  lgssq  15488  lgssq2  15489  lgsdirnn0  15495  lgsdinn0  15496  gausslemma2dlem6  15515  lgseisenlem1  15518  lgseisenlem3  15520  lgseisenlem4  15521  lgsquadlem1  15525  lgsquad2  15531  2sqlem3  15565  bj-charfundcALT  15707  nninfsellemeqinf  15915  refeq  15929