Theorem 3eqtr4d 2277

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

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 2216

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

This theorem is referenced by:  fnsnfv  5741  fvco2  5751  resfunexg  5910  fcof1  5962  fliftfun  5975  caovdir2d  6239  caov32d  6243  caov31d  6245  caov4d  6247  caovlem2d  6255  f1o3d  6271  caofcom  6306  caofdig  6309  cnvf1olem  6433  tfrlem1  6552  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  frecrdg  6652  oav2  6709  omv2  6711  omsuc  6718  nnmsucr  6734  ecovicom  6890  ecoviass  6892  ecovidi  6894  nnnninfeq  7432  nninfwlpoimlemg  7479  carden2bex  7499  addcompig  7660  addasspig  7661  mulcompig  7662  mulasspig  7663  distrpig  7664  addassnqg  7713  addnq0mo  7778  mulnq0mo  7779  nqnq0a  7785  nqnq0m  7786  distrnq0  7790  mulcomnq0  7791  addassnq0  7793  addcmpblnr  8070  mulcmpblnrlemg  8071  addsrmo  8074  mulsrmo  8075  ltsrprg  8078  recexgt0sr  8104  mulgt0sr  8109  mulextsr1lem  8111  addcnsrec  8173  mulcnsrec  8174  pitonnlem2  8178  recidpirqlemcalc  8188  axaddcom  8201  adddir  8281  mul32  8419  mul31  8420  add32  8448  add4  8450  sub32  8523  sub4  8534  subdir  8676  mulneg2  8686  mulreim  8895  apadd1  8899  apneg  8902  divassap  8981  divdirap  8988  divmul13ap  9006  divmul24ap  9007  divdiv32ap  9011  conjmulap  9020  zeo  9701  xaddcom  10213  xnegdi  10220  xaddass  10221  xaddass2  10222  xpncan  10223  xadd4d  10237  lincmb01cmp  10355  iccf1o  10357  flhalf  10686  modqvalp1  10729  modqdi  10778  modqsubdir  10779  frecuzrdgg  10802  seq3shft2  10867  seqshft2g  10868  seq3caopr3  10877  seqcaopr3g  10878  seq3caopr  10881  seqcaoprg  10882  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seq3f1olemqsum  10899  seqf1oglem2a  10904  seqf1oglem2  10906  seqf1og  10907  seq3homo  10913  seqfeq3  10915  seqhomog  10916  seqfeq4g  10917  seq3distr  10918  expp1  10932  expnegap0  10933  expaddzaplem  10968  expaddzap  10969  expmulzap  10971  sqneg  10984  sqdivap  10989  subsq2  11033  binom2  11037  modqexp  11053  facp1  11117  bcm1k  11147  bcp1n  11148  bcval5  11150  omgadd  11191  hashun  11194  hashxp  11216  hashfibclem  11231  csbwrdg  11279  ccatass  11321  lswccatn0lsw  11324  swrdlsw  11386  swrdswrd  11422  wrd2ind  11440  swrdccatin1  11442  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12lem3  11449  pfxccatpfx1  11453  swrdccat3blem  11456  cats1catd  11485  shftfibg  11530  shftfib  11533  shftval  11535  2shfti  11541  seq3shft  11548  crre  11567  remim  11570  mulreap  11574  reneg  11578  readd  11579  remullem  11581  redivap  11584  imneg  11586  imadd  11587  imdivap  11591  cjcj  11593  cjadd  11594  cjmulrcl  11597  cjneg  11600  imval2  11604  resqrexlemcalc1  11724  absneg  11760  sqabsadd  11765  sqabssub  11766  absmul  11779  absresq  11788  absexp  11789  absexpzap  11790  bdtrilem  11949  xrmaxiflemcom  11959  xrmaxadd  11971  xrminrecl  11983  xrminadd  11985  serf0  12062  summodclem3  12091  fsum3  12098  isumss  12102  fisumss  12103  fsumadd  12117  isummulc1  12138  isumdivapc  12139  fsum2dlemstep  12145  fisumcom2  12149  fisum0diag2  12158  fsummulc2  12159  fsummulc1  12160  fsumdivapc  12161  fsumconst  12165  telfsumo  12177  fsumparts  12181  binomlem  12194  isumshft  12201  arisum2  12210  geolim  12222  geo2sum  12225  geo2lim  12227  cvgratnnlemseq  12237  cvgratz  12243  mertenslem2  12247  prodfrecap  12257  prodfdivap  12258  prodmodclem2a  12287  fprodntrivap  12295  fprodssdc  12301  fprodmul  12302  fprodabs  12327  fprod2dlemstep  12333  fprodcom2fi  12337  fprodrec  12340  efcllemp  12369  efcj  12384  efexp  12393  resinval  12426  recosval  12427  cosneg  12438  efival  12443  sinadd  12447  cosadd  12448  addcos  12457  sin2t  12460  cos2t  12461  dvdsmodexp  12506  odd2np1lem  12583  oexpneg  12588  neggcd  12704  gcdabs2  12711  mulgcd  12737  mulgcdr  12739  gcddiv  12740  rplpwr  12748  eucalgval  12776  eucalginv  12778  eucalg  12781  neglcm  12797  lcmgcd  12800  mulgcddvds  12816  qredeu  12819  nn0gcdsq  12922  phimullem  12947  prmdiv  12957  coprimeprodsq  12980  pythagtriplem1  12988  pythagtriplem3  12990  pythagtriplem4  12991  pythagtriplem12  12998  pceulem  13017  pceu  13018  pcqmul  13026  pcexp  13032  pcneg  13048  pcadd  13063  pcmpt  13066  pcmpt2  13067  pcbc  13074  4sqlem7  13107  4sqlem10  13110  mul4sqlem  13116  4sqlem11  13124  ballotfilemfp1  13175  ballotfilemieq  13204  ballotfilemgun  13212  ballotfilemfrc  13214  ennnfonelemp1  13241  setsabsd  13335  setscom  13336  ressbasd  13364  strressid  13368  ressinbasd  13371  ressressg  13372  ressplusgd  13426  imasival  13570  qusin  13590  fvprif  13607  xpsfeq  13609  grpidpropdg  13637  gsumpropd  13655  gsumpropd2  13656  gsumress  13658  mnd32g  13688  mnd4g  13690  imasmnd2  13707  0mhm  13741  resmhm  13742  mhmco  13745  gsumwmhm  13753  grpinvcnv  13823  grpinvpropdg  13830  grpinvsub  13837  grpaddsubass  13845  grpsubpropdg  13859  grpsubpropd2  13860  imasgrp2  13863  imasgrp  13864  qusgrp2  13866  mulgnnp1  13883  mulgnegnn  13885  mulgaddcom  13899  mulginvcom  13900  mulgnndir  13904  mulgnn0ass  13911  mhmmulg  13916  mulgpropdg  13917  submmulg  13919  subginv  13934  subgsub  13939  subgmulg  13941  eqglact  13978  ghmsub  14004  ghmmulg  14009  resghm  14013  ghmeql  14020  conjghm  14029  ablsub4  14066  ablsub32  14075  imasabl  14089  gsumfzreidx  14090  gsumfzmptfidmadd  14092  gsumfzconst  14094  gfsumval  14102  gsumshift  14105  prdsval  14115  prdssgrpd  14133  prdsidlem  14135  prdsmndd  14136  prdsinvlem  14138  pwsplusgval  14150  pwsmulrval  14151  pws0g  14155  pwsinvg  14157  pwssub  14158  mgpress  14170  rngsubdi  14190  rngsubdir  14191  imasrng  14195  dfur2g  14205  srgass  14214  srgmulgass  14232  srgpcomp  14233  srglmhm  14236  srgrmhm  14237  crngcom  14257  ringass  14259  ringcom  14274  ringsubdi  14299  ringsubdir  14300  mulgass2  14301  ringlghm  14304  ringrghm  14305  imasring  14307  opprrng  14320  opprring  14322  oppr0g  14325  oppr1g  14326  opprnegg  14327  mulgass3  14329  dvdsrvald  14338  unitlinv  14371  unitrinv  14372  dvrfvald  14378  dvrass  14384  dvrdir  14388  rdivmuldivd  14389  rngidpropdg  14391  dvdsrpropdg  14392  unitpropdg  14393  invrpropdg  14394  rhm1  14412  rhmopp  14421  subrguss  14482  subrginv  14483  subrgdv  14484  rrgsupp  14512  aprprop  14539  opprdrng  14558  lmodcom  14607  lmodsubdir  14619  rmodislmod  14625  lsppropd  14706  srascag  14716  sravscag  14717  ixpsnbasval  14740  rsp0  14767  lidlrsppropdg  14769  rnglidlmsgrp  14771  gsumfzfsumlemm  14861  expghmap  14881  mulgghm2  14882  mulgrhm  14883  zlmlemg  14902  zlmsca  14906  znle  14911  psrbasg  14955  psrplusgg  14959  psrlinv  14965  tgdom  15063  txbasval  15258  cnmpt11  15274  cnmpt21  15282  setsmsbasg  15470  bdbl  15494  dvmulxxbr  15693  dvimulf  15697  dvcj  15700  dvfre  15701  dvrecap  15704  dvmptc  15708  dvmptfsum  15716  dvef  15718  plyaddlem1  15738  plyrecj  15754  dvply1  15756  sinperlem  15799  coshalfpip  15813  ptolemy  15815  tangtx  15829  relogef  15855  rpcxpadd  15896  rpmulcxp  15900  rpdivcxp  15902  cxpmul  15903  rpcxpmul2  15904  abscxp  15906  rpcxpsqrt  15913  rpabscxpbnd  15931  rplogbreexp  15944  rprelogbmul  15946  rprelogbdiv  15948  pellexlem3  15973  1sgmprm  15988  perfect1  15992  perfectlem2  15994  perfect  15995  lgsneg  16023  lgsmod  16025  lgsdir2  16032  lgsdirprm  16033  lgsdir  16034  lgsdi  16036  lgssq  16039  lgssq2  16040  lgsdirnn0  16046  lgsdinn0  16047  gausslemma2dlem6  16066  lgseisenlem1  16069  lgseisenlem3  16071  lgseisenlem4  16072  lgsquadlem1  16076  lgsquad2  16082  2sqlem3  16116  setsiedg  16173  vtxdeqd  16417  vtxdfifiun  16418  trlsegvdegfi  16588  depindlem3  16629  bj-charfundcALT  16705  nninfsellemeqinf  16920  refeq  16934