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  5632  fvco2  5642  resfunexg  5795  fcof1  5842  fliftfun  5855  caovdir2d  6113  caov32d  6117  caov31d  6119  caov4d  6121  caovlem2d  6129  caofcom  6179  caofdig  6182  cnvf1olem  6300  tfrlem1  6384  tfrlemisucaccv  6401  tfr1onlemsucaccv  6417  tfrcllemsucaccv  6430  frecrdg  6484  oav2  6539  omv2  6541  omsuc  6548  nnmsucr  6564  ecovicom  6720  ecoviass  6722  ecovidi  6724  nnnninfeq  7212  nninfwlpoimlemg  7259  carden2bex  7279  addcompig  7424  addasspig  7425  mulcompig  7426  mulasspig  7427  distrpig  7428  addassnqg  7477  addnq0mo  7542  mulnq0mo  7543  nqnq0a  7549  nqnq0m  7550  distrnq0  7554  mulcomnq0  7555  addassnq0  7557  addcmpblnr  7834  mulcmpblnrlemg  7835  addsrmo  7838  mulsrmo  7839  ltsrprg  7842  recexgt0sr  7868  mulgt0sr  7873  mulextsr1lem  7875  addcnsrec  7937  mulcnsrec  7938  pitonnlem2  7942  recidpirqlemcalc  7952  axaddcom  7965  adddir  8045  mul32  8184  mul31  8185  add32  8213  add4  8215  sub32  8288  sub4  8299  subdir  8440  mulneg2  8450  mulreim  8659  apadd1  8663  apneg  8666  divassap  8745  divdirap  8752  divmul13ap  8770  divmul24ap  8771  divdiv32ap  8775  conjmulap  8784  zeo  9460  xaddcom  9965  xnegdi  9972  xaddass  9973  xaddass2  9974  xpncan  9975  xadd4d  9989  lincmb01cmp  10107  iccf1o  10108  flhalf  10426  modqvalp1  10469  modqdi  10518  modqsubdir  10519  frecuzrdgg  10542  seq3shft2  10607  seqshft2g  10608  seq3caopr3  10617  seqcaopr3g  10618  seq3caopr  10621  seqcaoprg  10622  seq3f1olemqsumkj  10637  seq3f1olemqsumk  10638  seq3f1olemqsum  10639  seqf1oglem2a  10644  seqf1oglem2  10646  seqf1og  10647  seq3homo  10653  seqfeq3  10655  seqhomog  10656  seqfeq4g  10657  seq3distr  10658  expp1  10672  expnegap0  10673  expaddzaplem  10708  expaddzap  10709  expmulzap  10711  sqneg  10724  sqdivap  10729  subsq2  10773  binom2  10777  modqexp  10792  facp1  10856  bcm1k  10886  bcp1n  10887  bcval5  10889  omgadd  10928  hashun  10931  hashxp  10952  csbwrdg  10998  ccatass  11039  lswccatn0lsw  11042  shftfibg  11050  shftfib  11053  shftval  11055  2shfti  11061  seq3shft  11068  crre  11087  remim  11090  mulreap  11094  reneg  11098  readd  11099  remullem  11101  redivap  11104  imneg  11106  imadd  11107  imdivap  11111  cjcj  11113  cjadd  11114  cjmulrcl  11117  cjneg  11120  imval2  11124  resqrexlemcalc1  11244  absneg  11280  sqabsadd  11285  sqabssub  11286  absmul  11299  absresq  11308  absexp  11309  absexpzap  11310  bdtrilem  11469  xrmaxiflemcom  11479  xrmaxadd  11491  xrminrecl  11503  xrminadd  11505  serf0  11582  summodclem3  11610  fsum3  11617  isumss  11621  fisumss  11622  fsumadd  11636  isummulc1  11657  isumdivapc  11658  fsum2dlemstep  11664  fisumcom2  11668  fisum0diag2  11677  fsummulc2  11678  fsummulc1  11679  fsumdivapc  11680  fsumconst  11684  telfsumo  11696  fsumparts  11700  binomlem  11713  isumshft  11720  arisum2  11729  geolim  11741  geo2sum  11744  geo2lim  11746  cvgratnnlemseq  11756  cvgratz  11762  mertenslem2  11766  prodfrecap  11776  prodfdivap  11777  prodmodclem2a  11806  fprodntrivap  11814  fprodssdc  11820  fprodmul  11821  fprodabs  11846  fprod2dlemstep  11852  fprodcom2fi  11856  fprodrec  11859  efcllemp  11888  efcj  11903  efexp  11912  resinval  11945  recosval  11946  cosneg  11957  efival  11962  sinadd  11966  cosadd  11967  addcos  11976  sin2t  11979  cos2t  11980  dvdsmodexp  12025  odd2np1lem  12102  oexpneg  12107  neggcd  12223  gcdabs2  12230  mulgcd  12256  mulgcdr  12258  gcddiv  12259  rplpwr  12267  eucalgval  12295  eucalginv  12297  eucalg  12300  neglcm  12316  lcmgcd  12319  mulgcddvds  12335  qredeu  12338  nn0gcdsq  12441  phimullem  12466  prmdiv  12476  coprimeprodsq  12499  pythagtriplem1  12507  pythagtriplem3  12509  pythagtriplem4  12510  pythagtriplem12  12517  pceulem  12536  pceu  12537  pcqmul  12545  pcexp  12551  pcneg  12567  pcadd  12582  pcmpt  12585  pcmpt2  12586  pcbc  12593  4sqlem7  12626  4sqlem10  12629  mul4sqlem  12635  4sqlem11  12643  ennnfonelemp1  12696  setsabsd  12790  setscom  12791  ressbasd  12818  strressid  12822  ressinbasd  12825  ressressg  12826  ressplusgd  12879  prdsval  13023  pwsplusgval  13045  pwsmulrval  13046  imasival  13056  qusin  13076  fvprif  13093  xpsfeq  13095  grpidpropdg  13124  gsumpropd  13142  gsumpropd2  13143  gsumress  13145  prdssgrpd  13165  mnd32g  13177  mnd4g  13179  prdsidlem  13197  prdsmndd  13198  pws0g  13201  imasmnd2  13202  0mhm  13236  resmhm  13237  mhmco  13240  gsumwmhm  13248  grpinvcnv  13318  grpinvpropdg  13325  grpinvsub  13332  grpaddsubass  13340  grpsubpropdg  13354  grpsubpropd2  13355  prdsinvlem  13358  pwsinvg  13362  pwssub  13363  imasgrp2  13364  imasgrp  13365  qusgrp2  13367  mulgnnp1  13384  mulgnegnn  13386  mulgaddcom  13400  mulginvcom  13401  mulgnndir  13405  mulgnn0ass  13412  mhmmulg  13417  mulgpropdg  13418  submmulg  13420  subginv  13435  subgsub  13440  subgmulg  13442  eqglact  13479  ghmsub  13505  ghmmulg  13510  resghm  13514  ghmeql  13521  conjghm  13530  ablsub4  13567  ablsub32  13576  imasabl  13590  gsumfzreidx  13591  gsumfzmptfidmadd  13593  gsumfzconst  13595  mgpress  13611  rngsubdi  13631  rngsubdir  13632  imasrng  13636  dfur2g  13642  srgass  13651  srgmulgass  13669  srgpcomp  13670  srglmhm  13673  srgrmhm  13674  crngcom  13694  ringass  13696  ringcom  13711  ringsubdi  13736  ringsubdir  13737  mulgass2  13738  ringlghm  13741  ringrghm  13742  imasring  13744  opprrng  13757  opprring  13759  oppr0g  13761  oppr1g  13762  opprnegg  13763  mulgass3  13765  dvdsrvald  13773  unitlinv  13806  unitrinv  13807  dvrfvald  13813  dvrass  13819  dvrdir  13823  rdivmuldivd  13824  rngidpropdg  13826  dvdsrpropdg  13827  unitpropdg  13828  invrpropdg  13829  rhm1  13847  rhmopp  13856  subrguss  13916  subrginv  13917  subrgdv  13918  lmodcom  14013  lmodsubdir  14025  rmodislmod  14031  lsppropd  14112  srascag  14122  sravscag  14123  ixpsnbasval  14146  rsp0  14173  lidlrsppropdg  14175  rnglidlmsgrp  14177  gsumfzfsumlemm  14267  expghmap  14287  mulgghm2  14288  mulgrhm  14289  zlmlemg  14308  zlmsca  14312  znle  14317  psrbasg  14354  psrplusgg  14358  psrlinv  14364  tgdom  14462  txbasval  14657  cnmpt11  14673  cnmpt21  14681  setsmsbasg  14869  bdbl  14893  dvmulxxbr  15092  dvimulf  15096  dvcj  15099  dvfre  15100  dvrecap  15103  dvmptc  15107  dvmptfsum  15115  dvef  15117  plyaddlem1  15137  plyrecj  15153  dvply1  15155  sinperlem  15198  coshalfpip  15212  ptolemy  15214  tangtx  15228  relogef  15254  rpcxpadd  15295  rpmulcxp  15299  rpdivcxp  15301  cxpmul  15302  rpcxpmul2  15303  abscxp  15305  rpcxpsqrt  15312  rpabscxpbnd  15330  rplogbreexp  15343  rprelogbmul  15345  rprelogbdiv  15347  1sgmprm  15384  perfect1  15388  perfectlem2  15390  perfect  15391  lgsneg  15419  lgsmod  15421  lgsdir2  15428  lgsdirprm  15429  lgsdir  15430  lgsdi  15432  lgssq  15435  lgssq2  15436  lgsdirnn0  15442  lgsdinn0  15443  gausslemma2dlem6  15462  lgseisenlem1  15465  lgseisenlem3  15467  lgseisenlem4  15468  lgsquadlem1  15472  lgsquad2  15478  2sqlem3  15512  bj-charfundcALT  15609  nninfsellemeqinf  15817  refeq  15831