Theorem 3eqtr4rd 2808

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

Syntax hints:   → wi 4   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  csbun  4395  csbdif  4479  csbcnvgALTOLD  5860  csbres  5968  fimacnvinrn2  7053  f1ossf1o  7110  suppvalbr  8144  odi  8548  phplem2  9173  cantnfp1lem3  9635  cantnfp1  9636  cardidm  9917  ackbij2lem2  10195  ackbij2lem3  10196  divneg  11882  xadddilem  13297  xadddi2  13300  dfceil2  13849  modlt  13890  modmulnn  13899  seqcaopr3  14050  bcval5  14331  hashgadd  14390  hashun3  14397  hashmap  14448  seqcoll  14477  revccat  14779  cshwmodn  14808  2cshwcom  14829  cshimadifsn0  14843  revco  14847  cshco  14849  ofccat  14982  relexpsucl  15044  dfrtrclrec2  15071  cjreb  15150  recj  15151  imcj  15159  imval2  15178  sqrtmul  15286  absmax  15357  amgm2  15397  summolem2a  15742  fsumf1o  15750  sumsnf  15770  sumsplit  15795  fsummulc2  15811  binom  15860  bcxmas  15865  incexclem  15866  incexc  15867  expcnv  15894  pwdif  15898  cvgrat  15913  prodmolem3  15963  prodmolem2a  15964  fprodf1o  15976  prodsn  15992  prodsnf  15994  fprodabs  16004  binomfallfac  16071  fallfacval4  16073  bcfallfac  16074  ege2le3  16120  efaddlem  16123  eftlub  16141  tanval3  16166  tanneg  16180  cosmul  16205  cos01bnd  16218  demoivreALT  16233  flodddiv4  16449  absmulgcd  16583  nn0expgcd  16598  lcmfunsnlem2  16674  eulerthlem2  16817  phisum  16826  pythagtriplem14  16864  pythagtriplem19  16869  pcmul  16887  pcfac  16935  prmreclem6  16957  4sqlem12  16992  vdwlem6  17022  oppccatid  17751  curf2ndf  18279  oppcyon  18301  joincomALT  18431  meetcomALT  18433  pwsco1mhm  18866  sgrp2nmndlem4  18965  qusgrp2  19100  mulgnngsum  19121  mulgnn0p1  19127  mulgneg  19134  mulgnn0dir  19146  qusghm  19295  gaid  19339  symgval  19411  pmtrdifellem3  19518  psgnunilem2  19535  odmulg  19596  sylow1lem2  19639  sylow2a  19659  sylow3lem1  19667  efgredleme  19783  efgcpbllemb  19795  gsumzaddlem  19961  gsumconst  19974  gsumzmhm  19977  ablsimpgfindlem1  20149  srgpcomp  20268  srgbinom  20281  rdivmuldivd  20462  c0mgm  20508  c0mhm  20509  zrrnghm  20586  imadrhmcl  20846  lmodvsmmulgdi  20964  lmodsubdi  20986  rmodislmodlem  20996  0lmhm  21107  lspsneq  21192  qusrhm  21346  quscrng  21353  zringlpirlem3  21516  mulgrhm  21529  phssip  21710  frlmip  21830  frlmphl  21833  asclmulg  21954  resspsrmul  22027  evlsscasrng  22158  psdadd  22228  psdvsca  22229  psdmul  22231  psdpw  22235  psropprmul  22299  evls1scasrng  22402  mat1ghm  22543  mat1mhm  22544  1marepvmarrepid  22635  mdetrlin  22662  mdetrsca2  22664  mdetunilem7  22678  mdetunilem9  22680  mndifsplit  22696  maducoeval2  22700  smadiadetglem2  22732  decpmatmul  22832  pm2mpghm  22876  pm2mpmhmlem2  22879  cpmidgsum2  22939  ptbasfi  23641  ptuni  23654  alexsubALTlem3  24109  subgtgp  24165  tsmsxplem1  24213  xmsusp  24629  restmetu  24630  nminv  24681  nrginvrcnlem  24751  copco  25080  pcoass  25086  pi1bas  25100  pi1xfrf  25115  pi1xfr  25117  isclmp  25159  cph2subdi  25272  cphassr  25274  tcphcphlem1  25297  cphipval  25305  rrxip  25452  rrxnm  25453  pjthlem1  25499  ovolunlem1a  25558  ovolfs2  25633  uniiccdif  25640  ismbf  25690  itgaddlem2  25886  ditgswap  25921  ply1divex  26197  plyeq0lem  26270  plymullem1  26274  dgrcolem1  26333  dgrcolem2  26334  vieta1lem2  26375  elqaalem2  26384  elqaalem3  26385  aaliou3lem7  26413  ulmshft  26453  mulcxplem  26749  cxpmul2  26754  root1eq1  26820  cxpeq  26822  logbchbase  26836  cosangneg2d  26872  isosctrlem2  26884  angpieqvdlem  26893  chordthmlem3  26899  chordthmlem4  26900  chordthmlem5  26901  quad2  26904  dcubic2  26909  cubic2  26913  quart1  26921  scvxcvx  27050  igamlgam  27114  lgam1  27128  basellem9  27153  ppifl  27224  mumul  27245  sgmmul  27265  chtublem  27275  chpub  27284  logfacrlim  27288  dchrsum2  27332  sumdchr2  27334  bposlem9  27356  lgsdir2  27394  lgsdir  27396  lgsdi  27398  lgsdirnn0  27408  lgsdinn0  27409  lgsquad3  27451  2sqblem  27495  chpo1ub  27544  dchrmusum2  27558  dchrvmasumlem1  27559  dchrvmasum2if  27561  dchrisum0fmul  27570  rpvmasum2  27576  mulog2sumlem1  27598  vmalogdivsum2  27602  log2sumbnd  27608  selberg3lem1  27621  selberg4lem1  27624  pntrsumo1  27629  selbergr  27632  pntpbnd1  27650  pntlemk  27670  lesubsd  28189  mulsunif2lem  28262  divsasswd  28296  absmuls  28337  eucliddivs  28469  zcuts  28500  expsp1  28522  expadds  28528  pw2divsrecd  28540  pw2cut2  28555  bdayfinbndlem1  28560  tgbtwnconn1lem3  28743  mideulem2  28907  axlowdimlem16  29158  axcontlem8  29172  vtxval  29201  iedgval  29202  edgval  29250  vtxdgop  29671  finsumvtxdg2size  29751  lp1cycl  30354  ex-ind-dvds  30663  vsfval  30836  lnocoi  30960  nmblolbii  31002  ipasslem5  31038  hvsubid  31229  sshjval3  31557  pjhthlem1  31594  adjval  32093  unopf1o  32119  kbpj  32159  lnopmi  32203  nmcoplbi  32231  cnlnadjlem2  32271  adjadd  32296  branmfn  32308  pjtoi  32382  fconst7v  32822  ofoprabco  32866  supppreima  32893  sgnval2  32937  hashxpe  33009  ccatws1f1o  33129  splfv3  33136  xrsmulgzz  33187  mndractfo  33207  mndlactf1o  33208  mndractf1o  33209  gsumfs2d  33241  psgnfzto1stlem  33280  cycpmco2lem5  33310  cycpmco2lem6  33311  cyc3co2  33320  tocyccntz  33324  cyc3genpmlem  33331  cyc3conja  33337  archiabllem1a  33371  gsumvsca1  33406  gsumvsca2  33407  elrgspnlem2  33424  elrgspnsubrunlem1  33428  rloccring  33452  imaslmod  33539  elrspunidl  33614  mxidlirredi  33659  opprabs  33670  qsdrngi  33683  1arithidomlem1  33731  1arithidomlem2  33732  zringfrac  33750  ressply1evls1  33761  deg1prod  33779  psrbasfsupp  33808  selvply1rhmlem4  33820  mplvrpmga  33842  esplyind  33872  vietalem  33876  vieta  33877  ply1degltdimlem  33919  fedgmullem1  33926  fldextrspunlsplem  33970  extdgfialglem2  33990  algextdeglem4  34017  constrconj  34042  constrdircl  34062  constrremulcl  34064  constrimcl  34067  constrresqrtcl  34074  cos9thpiminplylem2  34080  submat1n  34102  submatres  34103  madjusmdetlem3  34126  xrge0iifhom  34234  qqhval2lem  34278  qqhrhm  34286  qqhucn  34289  esumsnf  34361  measvunilem0  34510  carsgclctunlem1  34614  ballotlemfp1  34789  ballotlemsf1o  34811  signstfveq0  34871  breprexplemc  34926  breprexp  34927  breprexpnat  34928  circlemeth  34934  logdivsqrle  34944  hgt750lema  34951  revwlk  35475  cvmlift3lem2  35670  cvmlift3lem4  35672  cvmlift3lem5  35673  cvmlift3lem6  35674  cvmlift3lem9  35677  elmrsubrn  35870  bccolsum  36089  bj-bary1lem  37802  qdiff  37819  finixpnum  38104  poimirlem4  38123  poimirlem16  38135  poimirlem19  38138  poimirlem25  38144  mblfinlem3  38158  dvtan  38169  itg2addnc  38173  itgaddnclem2  38178  ftc1anclem6  38197  areacirclem5  38211  areacirc  38212  upixp  38228  prdsbnd2  38294  ismrer1  38337  rngoneglmul  38442  rngoisocnv  38480  ecun  38892  islshpsm  39604  lshpnel2N  39609  lfl0f  39693  ldualvsdi1  39767  ldualgrplem  39769  cmtcomlemN  39872  cvlsupr8  39973  pmodl42N  40475  pmapjat1  40477  llnmod2i2  40487  dalawlem2  40496  pmapj2N  40553  idltrn  40774  cdlemc6  40820  cdleme20d  40936  cdleme22e  40968  cdleme22eALTN  40969  cdleme35b  41074  cdleme48fvg  41124  cdlemg4d  41237  cdlemg8a  41251  cdlemg42  41353  cdlemg47a  41358  tendodi1  41408  tendodi2  41409  cdlemk4  41458  cdlemk21N  41497  cdlemk22  41517  cdlemky  41550  cdlemk53b  41580  cdlemk53  41581  cdlemkyyN  41586  erngdvlem3-rN  41622  tendocnv  41645  dia1dim2  41686  dicvaddcl  41814  dihglblem3N  41919  dihmeetlem4preN  41930  dihmeet2  41970  lcfl7lem  42123  baerlem3lem1  42331  baerlem5alem1  42332  mapdh6bN  42361  mapdh6cN  42362  mapdh6dN  42363  hdmap1l6b  42435  hdmap1l6c  42436  hdmap1l6d  42437  hdmap14lem13  42504  ofun  42854  rediv23d  43070  grpcominv1  43130  evlselv  43171  flt4lem7  43241  3cubeslem2  43266  3cubeslem3r  43268  3cubeslem4  43270  pellexlem2  43407  rmxyneg  43497  oddcomabszz  43521  acongeq  43560  hausgraph  43782  onsupnmax  43805  tfsconcatrev  43925  naddass1  43970  fsovrfovd  44585  inductionexd  44731  expgrowth  44911  binomcxplemwb  44924  binomcxplemnn0  44925  binomcxplemnotnn0  44932  sumsnd  45606  restuni4  45699  fmuldfeqlem1  46158  cncfmptss  46163  climexp  46181  dvresntr  46492  stoweidlem17  46591  wallispi  46644  dirkertrigeq  46675  dirkercncflem2  46678  fourierdlem30  46711  fourierdlem41  46722  fourierdlem81  46761  fourierdlem103  46783  sge0xp  47003  sge0isummpt2  47006  isomennd  47105  vonioolem1  47254  sigarperm  47434  sin3t  47465  sin5tlem5  47471  fcores  47661  imasetpreimafvbijlemfo  48011  fundcmpsurbijinjpreimafv  48013  fundcmpsurinjimaid  48017  prprspr2  48124  ppivalnn  48241  opoeALTV  48305  uhgrimisgrgric  48553  isubgr3stgrlem2  48589  cznrng  48883  rngchomrnghmresALTV  48901  fdmdifeqresdif  48964  lincsum  49051  lincscm  49052  lmod1lem4  49112  blennngt2o2  49214  blennn0e2  49216  tposideq  49509  topdlat  49625  sectpropdlem  49657  invpropdlem  49659  isopropdlem  49661  imaidfu  49731  imasubc  49772  natoppf  49850  swapfid  49900  swapfcoa  49902  fucoppcid  50029  fucoppcco  50030  oppfdiag1  50035  diag1f1olem  50154  oppgoppchom  50211  oppgoppcco  50212  oppgoppcid  50213  2arwcat  50221  reccot  50379  rectan  50380  cotsqcscsq  50383  amgmlemALT  50424