Theorem 3eqtr4rd 2811

Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)

Hypotheses

Ref	Expression
3eqtr4d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3eqtr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3eqtr4rd	⊢ (𝜑 → 𝐷 = 𝐶)

Proof of Theorem 3eqtr4rd

Step	Hyp	Ref	Expression
1		3eqtr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
2		3eqtr4d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	eqtr4d 2803	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
4		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
5	3, 4	eqtr4d 2803	1 ⊢ (𝜑 → 𝐷 = 𝐶)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  csbun  4406  csbdif  4488  csbcnvgALTOLD  5876  csbres  5983  fimacnvinrn2  7071  f1ossf1o  7128  suppvalbr  8166  odi  8570  phplem2  9196  cantnfp1lem3  9656  cantnfp1  9657  cardidm  9961  ackbij2lem2  10238  ackbij2lem3  10239  divneg  11923  xadddilem  13338  xadddi2  13341  dfceil2  13892  modlt  13933  modmulnn  13942  seqcaopr3  14093  bcval5  14374  hashgadd  14433  hashun3  14440  hashmap  14492  seqcoll  14521  revccat  14827  cshwmodn  14858  2cshwcom  14879  cshimadifsn0  14893  revco  14897  cshco  14899  ofccat  15032  relexpsucl  15094  dfrtrclrec2  15121  cjreb  15200  recj  15201  imcj  15209  imval2  15228  sqrtmul  15336  absmax  15407  amgm2  15447  summolem2a  15791  fsumf1o  15799  sumsnf  15819  sumsplit  15844  fsummulc2  15860  binom  15909  bcxmas  15914  incexclem  15915  incexc  15916  expcnv  15943  pwdif  15947  cvgrat  15962  prodmolem3  16012  prodmolem2a  16013  fprodf1o  16025  prodsn  16041  prodsnf  16043  fprodabs  16053  binomfallfac  16119  fallfacval4  16121  bcfallfac  16122  ege2le3  16168  efaddlem  16171  eftlub  16189  tanval3  16214  tanneg  16228  cosmul  16253  cos01bnd  16266  demoivreALT  16281  flodddiv4  16497  absmulgcd  16631  nn0expgcd  16646  lcmfunsnlem2  16722  eulerthlem2  16865  phisum  16874  pythagtriplem14  16912  pythagtriplem19  16917  pcmul  16935  pcfac  16983  prmreclem6  17005  4sqlem12  17040  vdwlem6  17070  oppccatid  17799  curf2ndf  18327  oppcyon  18349  joincomALT  18479  meetcomALT  18481  pwsco1mhm  18930  sgrp2nmndlem4  19029  qusgrp2  19170  mulgnngsum  19191  mulgnn0p1  19197  mulgneg  19204  mulgnn0dir  19216  qusghm  19371  gaid  19415  symgval  19487  pmtrdifellem3  19594  psgnunilem2  19611  odmulg  19672  sylow1lem2  19715  sylow2a  19735  sylow3lem1  19743  efgredleme  19859  efgcpbllemb  19871  gsumzaddlem  20037  gsumconst  20050  gsumzmhm  20053  ablsimpgfindlem1  20225  srgpcomp  20346  srgbinom  20359  rdivmuldivd  20543  c0mgm  20589  c0mhm  20590  zrrnghm  20687  imadrhmcl  20952  lmodvsmmulgdi  21070  lmodsubdi  21092  rmodislmodlem  21102  0lmhm  21213  lspsneq  21298  qusrhm  21467  quscrng  21475  zringlpirlem3  21666  mulgrhm  21679  phssip  21860  frlmip  21980  frlmphl  21983  asclmulg  22104  resspsrmul  22177  evlsscasrng  22308  psdadd  22378  psdvsca  22379  psdmul  22381  psdpw  22385  psropprmul  22449  evls1scasrng  22551  mat1ghm  22692  mat1mhm  22693  1marepvmarrepid  22784  mdetrlin  22811  mdetrsca2  22813  mdetunilem7  22827  mdetunilem9  22829  mndifsplit  22845  maducoeval2  22849  smadiadetglem2  22881  decpmatmul  22981  pm2mpghm  23025  pm2mpmhmlem2  23028  cpmidgsum2  23088  ptbasfi  23791  ptuni  23804  alexsubALTlem3  24259  subgtgp  24315  tsmsxplem1  24363  xmsusp  24779  restmetu  24780  nminv  24831  nrginvrcnlem  24901  copco  25230  pcoass  25236  pi1bas  25250  pi1xfrf  25265  pi1xfr  25267  isclmp  25309  cph2subdi  25422  cphassr  25424  tcphcphlem1  25447  cphipval  25455  rrxip  25602  rrxnm  25603  pjthlem1  25649  ovolunlem1a  25708  ovolfs2  25783  uniiccdif  25790  ismbf  25840  itgaddlem2  26036  ditgswap  26071  ply1divex  26347  plyeq0lem  26420  plymullem1  26424  dgrcolem1  26483  dgrcolem2  26484  vieta1lem2  26525  elqaalem2  26534  elqaalem3  26535  aaliou3lem7  26565  ulmshft  26606  mulcxplem  26902  cxpmul2  26907  root1eq1  26973  cxpeq  26975  logbchbase  26989  cosangneg2d  27025  isosctrlem2  27037  angpieqvdlem  27046  chordthmlem3  27052  chordthmlem4  27053  chordthmlem5  27054  quad2  27057  dcubic2  27062  cubic2  27066  quart1  27074  scvxcvx  27203  igamlgam  27267  lgam1  27281  basellem9  27306  ppifl  27377  mumul  27398  sgmmul  27418  chtublem  27428  chpub  27437  logfacrlim  27441  dchrsum2  27485  sumdchr2  27487  bposlem9  27509  lgsdir2  27547  lgsdir  27549  lgsdi  27551  lgsdirnn0  27561  lgsdinn0  27562  lgsquad3  27604  2sqblem  27648  chpo1ub  27697  dchrmusum2  27711  dchrvmasumlem1  27712  dchrvmasum2if  27714  dchrisum0fmul  27723  rpvmasum2  27729  mulog2sumlem1  27751  vmalogdivsum2  27755  log2sumbnd  27761  selberg3lem1  27774  selberg4lem1  27777  pntrsumo1  27782  selbergr  27785  pntpbnd1  27803  pntlemk  27823  lesubsd  28342  mulsunif2lem  28415  divsasswd  28449  absmuls  28490  eucliddivs  28622  zcuts  28653  expsp1  28675  expadds  28681  pw2divsrecd  28693  pw2cut2  28708  bdayfinbndlem1  28713  tgbtwnconn1lem3  28896  mideulem2  29068  axlowdimlem16  29364  axcontlem8  29378  vtxval  29407  iedgval  29408  edgval  29456  vtxdgop  29880  finsumvtxdg2size  29960  revwlk  30096  lp1cycl  30572  ex-ind-dvds  30885  vsfval  31058  lnocoi  31182  nmblolbii  31224  ipasslem5  31260  hvsubid  31451  sshjval3  31779  pjhthlem1  31816  adjval  32315  unopf1o  32341  kbpj  32381  lnopmi  32425  nmcoplbi  32453  cnlnadjlem2  32493  adjadd  32518  branmfn  32530  pjtoi  32604  fconst7v  33038  ofoprabco  33082  supppreima  33109  sgnval2  33152  hashxpe  33224  ccatws1f1o  33339  splfv3  33344  xrsmulgzz  33395  mndractfo  33415  mndlactf1o  33416  mndractf1o  33417  gsumfs2d  33447  psgnfzto1stlem  33486  cycpmco2lem5  33516  cycpmco2lem6  33517  cyc3co2  33526  tocyccntz  33530  cyc3genpmlem  33537  cyc3conja  33543  archiabllem1a  33577  gsumvsca1  33612  gsumvsca2  33613  elrgspnlem2  33629  elrgspnsubrunlem1  33633  rloccring  33657  imaslmod  33739  elrspunidl  33802  mxidlirredi  33820  opprabs  33830  qsdrngi  33843  1arithidomlem1  33891  1arithidomlem2  33892  zringfrac  33910  ressply1evls1  33921  deg1prod  33939  psrbasfsupp  33967  selvply1rhmlem4  33979  mplvrpmga  34001  esplyind  34031  vietalem  34035  vieta  34036  ply1degltdimlem  34078  fedgmullem1  34085  fldextrspunlsplem  34129  extdgfialglem2  34149  algextdeglem4  34176  constrconj  34201  constrdircl  34221  constrremulcl  34223  constrimcl  34226  constrresqrtcl  34233  cos9thpiminplylem2  34239  submat1n  34261  submatres  34262  madjusmdetlem3  34285  xrge0iifhom  34393  qqhval2lem  34437  qqhrhm  34445  qqhucn  34448  esumsnf  34520  measvunilem0  34670  carsgclctunlem1  34774  ballotlemfp1  34949  ballotlemsf1o  34971  signstfveq0  35031  breprexplemc  35086  breprexp  35087  breprexpnat  35088  circlemeth  35094  logdivsqrle  35104  hgt750lema  35111  cvmlift3lem2  35851  cvmlift3lem4  35853  cvmlift3lem5  35854  cvmlift3lem6  35855  cvmlift3lem9  35858  elmrsubrn  36051  bccolsum  36270  bj-bary1lem  38013  qdiff  38030  finixpnum  38315  poimirlem4  38334  poimirlem16  38346  poimirlem19  38349  poimirlem25  38355  mblfinlem3  38369  dvtan  38380  itg2addnc  38384  itgaddnclem2  38389  ftc1anclem6  38408  areacirclem5  38422  areacirc  38423  upixp  38440  prdsbnd2  38506  ismrer1  38549  rngoneglmul  38654  rngoisocnv  38692  ecun  39102  islshpsm  39814  lshpnel2N  39819  lfl0f  39903  ldualvsdi1  39977  ldualgrplem  39979  cmtcomlemN  40082  cvlsupr8  40183  pmodl42N  40685  pmapjat1  40687  llnmod2i2  40697  dalawlem2  40706  pmapj2N  40763  idltrn  40984  cdlemc6  41030  cdleme20d  41146  cdleme22e  41178  cdleme22eALTN  41179  cdleme35b  41284  cdleme48fvg  41334  cdlemg4d  41447  cdlemg8a  41461  cdlemg42  41563  cdlemg47a  41568  tendodi1  41618  tendodi2  41619  cdlemk4  41668  cdlemk21N  41707  cdlemk22  41727  cdlemky  41760  cdlemk53b  41790  cdlemk53  41791  cdlemkyyN  41796  erngdvlem3-rN  41832  tendocnv  41855  dia1dim2  41896  dicvaddcl  42024  dihglblem3N  42129  dihmeetlem4preN  42140  dihmeet2  42180  lcfl7lem  42333  baerlem3lem1  42541  baerlem5alem1  42542  mapdh6bN  42571  mapdh6cN  42572  mapdh6dN  42573  hdmap1l6b  42645  hdmap1l6c  42646  hdmap1l6d  42647  hdmap14lem13  42714  ofun  43066  rediv23d  43282  grpcominv1  43342  evlselv  43381  flt4lem7  43451  3cubeslem2  43476  3cubeslem3r  43478  3cubeslem4  43480  pellexlem2  43617  rmxyneg  43707  oddcomabszz  43731  acongeq  43770  hausgraph  43992  onsupnmax  44015  tfsconcatrev  44135  naddass1  44180  fsovrfovd  44795  inductionexd  44941  expgrowth  45105  binomcxplemwb  45118  binomcxplemnn0  45119  binomcxplemnotnn0  45126  sumsnd  45806  restuni4  45899  fmuldfeqlem1  46358  cncfmptss  46363  climexp  46381  dvresntr  46692  stoweidlem17  46791  wallispi  46844  dirkertrigeq  46875  dirkercncflem2  46878  fourierdlem30  46911  fourierdlem41  46922  fourierdlem81  46961  fourierdlem103  46983  sge0xp  47203  sge0isummpt2  47206  isomennd  47305  vonioolem1  47454  sigarperm  47634  sin3t  47668  sin5tlem5  47674  fcores  47864  imasetpreimafvbijlemfo  48214  fundcmpsurbijinjpreimafv  48216  fundcmpsurinjimaid  48220  prprspr2  48327  ppivalnn  48444  opoeALTV  48508  uhgrimisgrgric  48756  isubgr3stgrlem2  48792  cznrng  49085  rngchomrnghmresALTV  49103  fdmdifeqresdif  49181  lincsum  49268  lincscm  49269  lmod1lem4  49329  blennngt2o2  49431  blennn0e2  49433  tposideq  49725  topdlat  49841  sectpropdlem  49873  invpropdlem  49875  isopropdlem  49877  imaidfu  49947  imasubc  49988  natoppf  50066  swapfid  50116  swapfcoa  50118  fucoppcid  50245  fucoppcco  50246  oppfdiag1  50251  diag1f1olem  50370  oppgoppchom  50427  oppgoppcco  50428  oppgoppcid  50429  2arwcat  50437  reccot  50595  rectan  50596  cotsqcscsq  50599  crosspaltd  50707  crossp3d  50708  amgmlemALT  50710