Theorem 3eqtr4rd 2809

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

Syntax hints:   → wi 4   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  csbun  4406  csbdif  4486  csbcnvgALTOLD  5874  csbres  5981  fimacnvinrn2  7067  f1ossf1o  7124  suppvalbr  8156  odi  8560  phplem2  9185  cantnfp1lem3  9645  cantnfp1  9646  cardidm  9941  ackbij2lem2  10218  ackbij2lem3  10219  divneg  11901  xadddilem  13315  xadddi2  13318  dfceil2  13868  modlt  13909  modmulnn  13918  seqcaopr3  14069  bcval5  14350  hashgadd  14409  hashun3  14416  hashmap  14468  seqcoll  14497  revccat  14799  cshwmodn  14828  2cshwcom  14849  cshimadifsn0  14863  revco  14867  cshco  14869  ofccat  15002  relexpsucl  15064  dfrtrclrec2  15091  cjreb  15170  recj  15171  imcj  15179  imval2  15198  sqrtmul  15306  absmax  15377  amgm2  15417  summolem2a  15762  fsumf1o  15770  sumsnf  15790  sumsplit  15815  fsummulc2  15831  binom  15880  bcxmas  15885  incexclem  15886  incexc  15887  expcnv  15914  pwdif  15918  cvgrat  15933  prodmolem3  15983  prodmolem2a  15984  fprodf1o  15996  prodsn  16012  prodsnf  16014  fprodabs  16024  binomfallfac  16090  fallfacval4  16092  bcfallfac  16093  ege2le3  16139  efaddlem  16142  eftlub  16160  tanval3  16185  tanneg  16199  cosmul  16224  cos01bnd  16237  demoivreALT  16252  flodddiv4  16468  absmulgcd  16602  nn0expgcd  16617  lcmfunsnlem2  16693  eulerthlem2  16836  phisum  16845  pythagtriplem14  16883  pythagtriplem19  16888  pcmul  16906  pcfac  16954  prmreclem6  16976  4sqlem12  17011  vdwlem6  17041  oppccatid  17770  curf2ndf  18298  oppcyon  18320  joincomALT  18450  meetcomALT  18452  pwsco1mhm  18886  sgrp2nmndlem4  18985  qusgrp2  19119  mulgnngsum  19140  mulgnn0p1  19146  mulgneg  19153  mulgnn0dir  19165  qusghm  19320  gaid  19364  symgval  19436  pmtrdifellem3  19543  psgnunilem2  19560  odmulg  19621  sylow1lem2  19664  sylow2a  19684  sylow3lem1  19692  efgredleme  19808  efgcpbllemb  19820  gsumzaddlem  19986  gsumconst  19999  gsumzmhm  20002  ablsimpgfindlem1  20174  srgpcomp  20295  srgbinom  20308  rdivmuldivd  20491  c0mgm  20537  c0mhm  20538  zrrnghm  20635  imadrhmcl  20900  lmodvsmmulgdi  21018  lmodsubdi  21040  rmodislmodlem  21050  0lmhm  21161  lspsneq  21246  qusrhm  21415  quscrng  21423  zringlpirlem3  21614  mulgrhm  21627  phssip  21808  frlmip  21928  frlmphl  21931  asclmulg  22052  resspsrmul  22125  evlsscasrng  22256  psdadd  22326  psdvsca  22327  psdmul  22329  psdpw  22333  psropprmul  22397  evls1scasrng  22499  mat1ghm  22640  mat1mhm  22641  1marepvmarrepid  22732  mdetrlin  22759  mdetrsca2  22761  mdetunilem7  22775  mdetunilem9  22777  mndifsplit  22793  maducoeval2  22797  smadiadetglem2  22829  decpmatmul  22929  pm2mpghm  22973  pm2mpmhmlem2  22976  cpmidgsum2  23036  ptbasfi  23738  ptuni  23751  alexsubALTlem3  24206  subgtgp  24262  tsmsxplem1  24310  xmsusp  24726  restmetu  24727  nminv  24778  nrginvrcnlem  24848  copco  25177  pcoass  25183  pi1bas  25197  pi1xfrf  25212  pi1xfr  25214  isclmp  25256  cph2subdi  25369  cphassr  25371  tcphcphlem1  25394  cphipval  25402  rrxip  25549  rrxnm  25550  pjthlem1  25596  ovolunlem1a  25655  ovolfs2  25730  uniiccdif  25737  ismbf  25787  itgaddlem2  25983  ditgswap  26018  ply1divex  26294  plyeq0lem  26367  plymullem1  26371  dgrcolem1  26430  dgrcolem2  26431  vieta1lem2  26472  elqaalem2  26481  elqaalem3  26482  aaliou3lem7  26512  ulmshft  26553  mulcxplem  26849  cxpmul2  26854  root1eq1  26920  cxpeq  26922  logbchbase  26936  cosangneg2d  26972  isosctrlem2  26984  angpieqvdlem  26993  chordthmlem3  26999  chordthmlem4  27000  chordthmlem5  27001  quad2  27004  dcubic2  27009  cubic2  27013  quart1  27021  scvxcvx  27150  igamlgam  27214  lgam1  27228  basellem9  27253  ppifl  27324  mumul  27345  sgmmul  27365  chtublem  27375  chpub  27384  logfacrlim  27388  dchrsum2  27432  sumdchr2  27434  bposlem9  27456  lgsdir2  27494  lgsdir  27496  lgsdi  27498  lgsdirnn0  27508  lgsdinn0  27509  lgsquad3  27551  2sqblem  27595  chpo1ub  27644  dchrmusum2  27658  dchrvmasumlem1  27659  dchrvmasum2if  27661  dchrisum0fmul  27670  rpvmasum2  27676  mulog2sumlem1  27698  vmalogdivsum2  27702  log2sumbnd  27708  selberg3lem1  27721  selberg4lem1  27724  pntrsumo1  27729  selbergr  27732  pntpbnd1  27750  pntlemk  27770  lesubsd  28289  mulsunif2lem  28362  divsasswd  28396  absmuls  28437  eucliddivs  28569  zcuts  28600  expsp1  28622  expadds  28628  pw2divsrecd  28640  pw2cut2  28655  bdayfinbndlem1  28660  tgbtwnconn1lem3  28843  mideulem2  29015  axlowdimlem16  29307  axcontlem8  29321  vtxval  29350  iedgval  29351  edgval  29399  vtxdgop  29820  finsumvtxdg2size  29900  lp1cycl  30503  ex-ind-dvds  30812  vsfval  30985  lnocoi  31109  nmblolbii  31151  ipasslem5  31187  hvsubid  31378  sshjval3  31706  pjhthlem1  31743  adjval  32242  unopf1o  32268  kbpj  32308  lnopmi  32352  nmcoplbi  32380  cnlnadjlem2  32420  adjadd  32445  branmfn  32457  pjtoi  32531  fconst7v  32965  ofoprabco  33009  supppreima  33036  sgnval2  33080  hashxpe  33152  ccatws1f1o  33271  splfv3  33278  xrsmulgzz  33329  mndractfo  33349  mndlactf1o  33350  mndractf1o  33351  gsumfs2d  33381  psgnfzto1stlem  33420  cycpmco2lem5  33450  cycpmco2lem6  33451  cyc3co2  33460  tocyccntz  33464  cyc3genpmlem  33471  cyc3conja  33477  archiabllem1a  33511  gsumvsca1  33546  gsumvsca2  33547  elrgspnlem2  33563  elrgspnsubrunlem1  33567  rloccring  33591  imaslmod  33673  elrspunidl  33736  mxidlirredi  33754  opprabs  33764  qsdrngi  33777  1arithidomlem1  33825  1arithidomlem2  33826  zringfrac  33844  ressply1evls1  33855  deg1prod  33873  psrbasfsupp  33901  selvply1rhmlem4  33913  mplvrpmga  33935  esplyind  33965  vietalem  33969  vieta  33970  ply1degltdimlem  34012  fedgmullem1  34019  fldextrspunlsplem  34063  extdgfialglem2  34083  algextdeglem4  34110  constrconj  34135  constrdircl  34155  constrremulcl  34157  constrimcl  34160  constrresqrtcl  34167  cos9thpiminplylem2  34173  submat1n  34195  submatres  34196  madjusmdetlem3  34219  xrge0iifhom  34327  qqhval2lem  34371  qqhrhm  34379  qqhucn  34382  esumsnf  34454  measvunilem0  34603  carsgclctunlem1  34707  ballotlemfp1  34882  ballotlemsf1o  34904  signstfveq0  34964  breprexplemc  35019  breprexp  35020  breprexpnat  35021  circlemeth  35027  logdivsqrle  35037  hgt750lema  35044  revwlk  35617  cvmlift3lem2  35812  cvmlift3lem4  35814  cvmlift3lem5  35815  cvmlift3lem6  35816  cvmlift3lem9  35819  elmrsubrn  36012  bccolsum  36231  bj-bary1lem  37974  qdiff  37991  finixpnum  38276  poimirlem4  38295  poimirlem16  38307  poimirlem19  38310  poimirlem25  38316  mblfinlem3  38330  dvtan  38341  itg2addnc  38345  itgaddnclem2  38350  ftc1anclem6  38369  areacirclem5  38383  areacirc  38384  upixp  38400  prdsbnd2  38466  ismrer1  38509  rngoneglmul  38614  rngoisocnv  38652  ecun  39062  islshpsm  39774  lshpnel2N  39779  lfl0f  39863  ldualvsdi1  39937  ldualgrplem  39939  cmtcomlemN  40042  cvlsupr8  40143  pmodl42N  40645  pmapjat1  40647  llnmod2i2  40657  dalawlem2  40666  pmapj2N  40723  idltrn  40944  cdlemc6  40990  cdleme20d  41106  cdleme22e  41138  cdleme22eALTN  41139  cdleme35b  41244  cdleme48fvg  41294  cdlemg4d  41407  cdlemg8a  41421  cdlemg42  41523  cdlemg47a  41528  tendodi1  41578  tendodi2  41579  cdlemk4  41628  cdlemk21N  41667  cdlemk22  41687  cdlemky  41720  cdlemk53b  41750  cdlemk53  41751  cdlemkyyN  41756  erngdvlem3-rN  41792  tendocnv  41815  dia1dim2  41856  dicvaddcl  41984  dihglblem3N  42089  dihmeetlem4preN  42100  dihmeet2  42140  lcfl7lem  42293  baerlem3lem1  42501  baerlem5alem1  42502  mapdh6bN  42531  mapdh6cN  42532  mapdh6dN  42533  hdmap1l6b  42605  hdmap1l6c  42606  hdmap1l6d  42607  hdmap14lem13  42674  ofun  43026  rediv23d  43242  grpcominv1  43302  evlselv  43341  flt4lem7  43411  3cubeslem2  43436  3cubeslem3r  43438  3cubeslem4  43440  pellexlem2  43577  rmxyneg  43667  oddcomabszz  43691  acongeq  43730  hausgraph  43952  onsupnmax  43975  tfsconcatrev  44095  naddass1  44140  fsovrfovd  44755  inductionexd  44901  expgrowth  45065  binomcxplemwb  45078  binomcxplemnn0  45079  binomcxplemnotnn0  45086  sumsnd  45766  restuni4  45859  fmuldfeqlem1  46318  cncfmptss  46323  climexp  46341  dvresntr  46652  stoweidlem17  46751  wallispi  46804  dirkertrigeq  46835  dirkercncflem2  46838  fourierdlem30  46871  fourierdlem41  46882  fourierdlem81  46921  fourierdlem103  46943  sge0xp  47163  sge0isummpt2  47166  isomennd  47265  vonioolem1  47414  sigarperm  47594  sin3t  47628  sin5tlem5  47634  fcores  47824  imasetpreimafvbijlemfo  48174  fundcmpsurbijinjpreimafv  48176  fundcmpsurinjimaid  48180  prprspr2  48287  ppivalnn  48404  opoeALTV  48468  uhgrimisgrgric  48716  isubgr3stgrlem2  48752  cznrng  49046  rngchomrnghmresALTV  49064  fdmdifeqresdif  49142  lincsum  49229  lincscm  49230  lmod1lem4  49290  blennngt2o2  49392  blennn0e2  49394  tposideq  49686  topdlat  49802  sectpropdlem  49834  invpropdlem  49836  isopropdlem  49838  imaidfu  49908  imasubc  49949  natoppf  50027  swapfid  50077  swapfcoa  50079  fucoppcid  50206  fucoppcco  50207  oppfdiag1  50212  diag1f1olem  50331  oppgoppchom  50388  oppgoppcco  50389  oppgoppcid  50390  2arwcat  50398  reccot  50556  rectan  50557  cotsqcscsq  50560  crosspalti  50667  amgmlemALT  50670