Theorem 3eqtr4d 2281

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  fnsnfv  5765  fvco2  5777  resfunexg  5939  fcof1  5992  fliftfun  6005  caovdir2d  6269  caov32d  6273  caov31d  6275  caov4d  6277  caovlem2d  6285  f1o3d  6301  caofcom  6337  caofdig  6340  cnvf1olem  6464  tfrlem1  6583  tfrlemisucaccv  6600  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  frecrdg  6683  oav2  6740  omv2  6742  omsuc  6749  nnmsucr  6765  ecovicom  6921  ecoviass  6923  ecovidi  6925  nnnninfeq  7474  nninfwlpoimlemg  7521  carden2bex  7541  addcompig  7702  addasspig  7703  mulcompig  7704  mulasspig  7705  distrpig  7706  addassnqg  7755  addnq0mo  7820  mulnq0mo  7821  nqnq0a  7827  nqnq0m  7828  distrnq0  7832  mulcomnq0  7833  addassnq0  7835  addcmpblnr  8112  mulcmpblnrlemg  8113  addsrmo  8116  mulsrmo  8117  ltsrprg  8120  recexgt0sr  8146  mulgt0sr  8151  mulextsr1lem  8153  addcnsrec  8215  mulcnsrec  8216  pitonnlem2  8220  recidpirqlemcalc  8230  axaddcom  8243  adddir  8323  mul32  8463  mul31  8464  add32  8492  add4  8494  sub32  8567  sub4  8578  subdir  8720  mulneg2  8730  mulreim  8940  apadd1  8944  apneg  8947  divassap  9028  divdirap  9035  divmul13ap  9053  divmul24ap  9054  divdiv32ap  9058  conjmulap  9067  zeo  9762  xaddcom  10280  xnegdi  10287  xaddass  10288  xaddass2  10289  xpncan  10290  xadd4d  10304  lincmb01cmp  10422  iccf1o  10424  flhalf  10758  modqvalp1  10801  modqdi  10850  modqsubdir  10851  frecuzrdgg  10874  seq3shft2  10939  seqshft2g  10940  seq3caopr3  10949  seqcaopr3g  10950  seq3caopr  10953  seqcaoprg  10954  seq3f1olemqsumkj  10969  seq3f1olemqsumk  10970  seq3f1olemqsum  10971  seqf1oglem2a  10976  seqf1oglem2  10978  seqf1og  10979  seq3homo  10985  seqfeq3  10987  seqhomog  10988  seqfeq4g  10989  seq3distr  10990  expp1  11004  expnegap0  11005  expaddzaplem  11040  expaddzap  11041  expmulzap  11043  sqneg  11056  sqdivap  11061  subsq2  11105  binom2  11109  modqexp  11125  facp1  11190  bcm1k  11220  bcp1n  11221  bcval5  11223  omgadd  11264  hashun  11267  hashxp  11289  hashfibclem  11304  hashf1  11309  csbwrdg  11356  ccatass  11398  lswccatn0lsw  11401  swrdlsw  11463  swrdswrd  11499  wrd2ind  11517  swrdccatin1  11519  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccatin12lem3  11526  pfxccatpfx1  11530  swrdccat3blem  11533  cats1catd  11562  shftfibg  11607  shftfib  11610  shftval  11612  2shfti  11618  seq3shft  11625  crre  11644  remim  11647  mulreap  11651  reneg  11655  readd  11656  remullem  11658  redivap  11661  imneg  11663  imadd  11664  imdivap  11668  cjcj  11670  cjadd  11671  cjmulrcl  11674  cjneg  11677  imval2  11681  resqrexlemcalc1  11802  absneg  11838  sqabsadd  11843  sqabssub  11844  absmul  11857  absresq  11867  absexp  11868  absexpzap  11869  bdtrilem  12030  xrmaxiflemcom  12040  xrmaxadd  12052  xrminrecl  12064  xrminadd  12066  serf0  12143  summodclem3  12172  fsum3  12179  isumss  12183  fisumss  12184  fsumadd  12198  isummulc1  12219  isumdivapc  12220  fsum2dlemstep  12226  fisumcom2  12230  fisum0diag2  12239  fsummulc2  12240  fsummulc1  12241  fsumdivapc  12242  fsumconst  12246  telfsumo  12258  fsumparts  12262  binomlem  12275  isumshft  12282  arisum2  12291  geolim  12303  geo2sum  12306  geo2lim  12308  cvgratnnlemseq  12318  cvgratz  12324  mertenslem2  12328  prodfrecap  12338  prodfdivap  12339  prodmodclem2a  12368  fprodntrivap  12376  fprodssdc  12382  fprodmul  12383  fprodabs  12408  fprod2dlemstep  12414  fprodcom2fi  12418  fprodrec  12421  efcllemp  12450  efcj  12465  efexp  12474  resinval  12507  recosval  12508  cosneg  12519  efival  12524  sinadd  12528  cosadd  12529  addcos  12538  sin2t  12541  cos2t  12542  dvdsmodexp  12587  odd2np1lem  12664  oexpneg  12669  neggcd  12785  gcdabs2  12792  mulgcd  12818  mulgcdr  12820  gcddiv  12821  rplpwr  12829  eucalgval  12857  eucalginv  12859  eucalg  12862  neglcm  12878  lcmgcd  12881  mulgcddvds  12897  qredeu  12900  nn0gcdsq  13005  phimullem  13032  prmdiv  13042  coprimeprodsq  13065  pythagtriplem1  13073  pythagtriplem3  13075  pythagtriplem4  13076  pythagtriplem12  13083  pceulem  13102  pceu  13103  pcqmul  13111  pcexp  13117  pcneg  13133  pcadd  13148  pcmpt  13151  pcmpt2  13152  pcbc  13159  4sqlem7  13192  4sqlem10  13195  mul4sqlem  13201  4sqlem11  13209  ballotfilemfp1  13289  ballotfilemieq  13318  ballotfilemgun  13326  ballotfilemfrc  13328  ennnfonelemp1  13355  setsabsd  13449  setscom  13450  ressbasd  13480  strressid  13484  ressinbasd  13487  ressressg  13488  ressplusgd  13542  imasival  13686  qusin  13706  fvprif  13723  xpsfeq  13725  grpidpropdg  13753  gzsumress  13771  mnd32g  13799  mnd4g  13801  imasmnd2  13818  0mhm  13852  resmhm  13853  mhmco  13856  gzsumwmhm  13862  grpinvcnv  13932  grpinvpropdg  13939  grpinvsub  13946  grpaddsubass  13954  grpsubpropdg  13968  grpsubpropd2  13969  imasgrp2  13972  imasgrp  13973  qusgrp2  13975  mulgnnp1  13992  mulgnegnn  13994  mulgaddcom  14008  mulginvcom  14009  mulgnndir  14013  mulgnn0ass  14020  mhmmulg  14025  mulgpropdg  14026  submmulg  14028  subginv  14043  subgsub  14048  subgmulg  14050  eqglact  14087  ghmsub  14113  ghmmulg  14118  resghm  14122  ghmeql  14129  conjghm  14138  ablsub4  14207  ablsub32  14216  imasabl  14230  gzsumreidx  14231  gzsumconst  14233  gzsumshift  14239  gsumvalfi  14242  gsumf1ofi  14250  gsummptfidmadd  14251  gsummptfidmsplitres  14255  gsumsplitfi  14256  gsumresfi  14263  gsummhmfi  14264  gsumconstcmn  14266  gsumressfi  14267  prdsval  14280  prdssgrpd  14298  prdsidlem  14300  prdsmndd  14301  prdsinvlem  14303  pwsplusgval  14315  pwsmulrval  14316  pws0g  14320  pwsinvg  14322  pwssub  14323  mgpress  14337  rngsubdi  14357  rngsubdir  14358  imasrng  14362  dfur2g  14373  srgass  14382  srgmulgass  14400  srgpcomp  14401  srglmhm  14404  srgrmhm  14405  crngcom  14425  ringass  14427  ringcom  14443  ringsubdi  14468  ringsubdir  14469  mulgass2  14470  ringlghm  14473  ringrghm  14474  imasring  14478  opprrng  14491  opprring  14493  oppr0g  14496  oppr1g  14497  opprnegg  14498  mulgass3  14500  dvdsrvald  14509  unitlinv  14542  unitrinv  14543  dvrfvald  14549  dvrass  14555  dvrdir  14559  rdivmuldivd  14560  rngidpropdg  14562  dvdsrpropdg  14563  unitpropdg  14564  invrpropdg  14565  rhm1  14583  rhmopp  14592  subrguss  14653  subrginv  14654  subrgdv  14655  rrgsupp  14683  aprprop  14710  opprdrng  14729  lmodcom  14779  lmodsubdir  14791  rmodislmod  14797  lsppropd  14878  srascag  14888  sravscag  14889  ixpsnbasval  14912  rsp0  14939  lidlrsppropdg  14941  rnglidlmsgrp  14943  gsumfsum  15032  expghmap  15051  mulgghm2  15052  mulgrhm  15053  zlmlemg  15072  zlmsca  15076  znle  15081  asclghm  15134  ascldimul  15140  assamulgscmlem1  15150  psrass1filem  15177  psrbasg  15178  psrplusgg  15182  psrlinv  15194  psrass1fi  15201  psrdifi  15202  psrdirfi  15203  tgdom  15298  txbasval  15493  cnmpt11  15509  cnmpt21  15517  setsmsbasg  15705  bdbl  15729  dvmulxxbr  15928  dvimulf  15932  dvcj  15935  dvfre  15936  dvrecap  15939  dvmptc  15943  dvmptfsum  15951  dvef  15953  plyaddlem1  15973  plyrecj  15989  dvply1  15991  sinperlem  16035  coshalfpip  16049  ptolemy  16051  tangtx  16065  relogef  16093  logfac  16126  rpcxpadd  16138  rpmulcxp  16142  rpdivcxp  16144  cxpmul  16145  rpcxpmul2  16146  rpcxpmul2z  16148  abscxp  16150  rpcxpsqrt  16157  rpabscxpbnd  16175  rplogbreexp  16189  rprelogbmul  16191  rprelogbdiv  16193  birthdaylem2  16226  pellexlem3  16231  chtqfl  16258  ppiprm  16259  ppinprm  16260  chtnprm  16262  prmorcht  16282  1sgmprm  16288  perfect1  16298  perfectlem2  16300  perfect  16301  bcmono  16304  bposlem9  16319  lgsneg  16348  lgsmod  16350  lgsdir2  16357  lgsdirprm  16358  lgsdir  16359  lgsdi  16361  lgssq  16364  lgssq2  16365  lgsdirnn0  16371  lgsdinn0  16372  gausslemma2dlem6  16391  lgseisenlem1  16394  lgseisenlem3  16396  lgseisenlem4  16397  lgsquadlem1  16401  lgsquad2  16407  2sqlem3  16441  setsiedg  16498  vtxdeqd  16742  vtxdfifiun  16743  trlsegvdegfi  16913  depindlem3  16954  bj-charfundcALT  17040  nninfsellemeqinf  17265  refeq  17279