Theorem 3eqtr4rd 2776

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

Syntax hints:   → wi 4   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717

This theorem is referenced by:  csbun  4440  csbdif  4529  csbcnvgALT  5887  csbres  5988  fimacnvinrn2  7081  f1ossf1o  7137  suppvalbr  8169  odi  8600  phplem2  9236  phplem4OLD  9248  cantnfp1lem3  9710  cantnfp1  9711  cardidm  9989  ackbij2lem2  10270  ackbij2lem3  10271  divneg  11944  xadddilem  13313  xadddi2  13316  dfceil2  13845  modlt  13886  modmulnn  13895  seqcaopr3  14043  bcval5  14321  hashgadd  14380  hashun3  14387  hashmap  14438  seqcoll  14469  revccat  14760  cshwmodn  14789  2cshwcom  14810  cshimadifsn0  14825  revco  14829  cshco  14831  ofccat  14960  relexpsucl  15022  dfrtrclrec2  15049  cjreb  15114  recj  15115  imcj  15123  imval2  15142  sqrtmul  15250  absmax  15320  amgm2  15360  summolem2a  15705  fsumf1o  15713  sumsnf  15733  sumsplit  15758  fsummulc2  15774  binom  15820  bcxmas  15825  incexclem  15826  incexc  15827  expcnv  15854  pwdif  15858  cvgrat  15873  prodmolem3  15921  prodmolem2a  15922  fprodf1o  15934  prodsn  15950  prodsnf  15952  fprodabs  15962  binomfallfac  16029  fallfacval4  16031  bcfallfac  16032  ege2le3  16078  efaddlem  16081  eftlub  16097  tanval3  16122  tanneg  16136  cosmul  16161  cos01bnd  16174  demoivreALT  16189  flodddiv4  16401  absmulgcd  16536  nn0expgcd  16551  lcmfunsnlem2  16627  eulerthlem2  16770  phisum  16778  pythagtriplem14  16816  pythagtriplem19  16821  pcmul  16839  pcfac  16887  prmreclem6  16909  4sqlem12  16944  vdwlem6  16974  oppccatid  17720  curf2ndf  18258  oppcyon  18280  joincomALT  18412  meetcomALT  18414  pwsco1mhm  18808  sgrp2nmndlem4  18904  qusgrp2  19038  mulgnngsum  19059  mulgnn0p1  19065  mulgneg  19072  mulgnn0dir  19084  qusghm  19235  gaid  19279  symgval  19352  pmtrdifellem3  19462  psgnunilem2  19479  odmulg  19540  sylow1lem2  19583  sylow2a  19603  sylow3lem1  19611  efgredleme  19727  efgcpbllemb  19739  gsumzaddlem  19905  gsumconst  19918  gsumzmhm  19921  ablsimpgfindlem1  20093  srgpcomp  20187  srgbinom  20200  rdivmuldivd  20381  c0mgm  20427  c0mhm  20428  zrrnghm  20502  imadrhmcl  20714  lmodvsmmulgdi  20809  lmodsubdi  20831  rmodislmodlem  20841  0lmhm  20954  lspsneq  21039  qusrhm  21200  quscrng  21207  zringlpirlem3  21424  mulgrhm  21437  phssip  21624  frlmip  21746  frlmphl  21749  asclmulg  21869  resspsrmul  21955  evlsscasrng  22082  psdadd  22127  psdvsca  22128  psdmul  22130  psropprmul  22197  evls1scasrng  22300  mat1ghm  22446  mat1mhm  22447  1marepvmarrepid  22538  mdetrlin  22565  mdetrsca2  22567  mdetunilem7  22581  mdetunilem9  22583  mndifsplit  22599  maducoeval2  22603  smadiadetglem2  22635  decpmatmul  22735  pm2mpghm  22779  pm2mpmhmlem2  22782  cpmidgsum2  22842  ptbasfi  23546  ptuni  23559  alexsubALTlem3  24014  subgtgp  24070  tsmsxplem1  24118  xmsusp  24539  restmetu  24540  nminv  24591  nrginvrcnlem  24669  copco  25006  pcoass  25012  pi1bas  25026  pi1xfrf  25041  pi1xfr  25043  isclmp  25085  cph2subdi  25199  cphassr  25201  tcphcphlem1  25224  cphipval  25232  rrxip  25379  rrxnm  25380  pjthlem1  25426  ovolunlem1a  25486  ovolfs2  25561  uniiccdif  25568  ismbf  25618  itgaddlem2  25814  ditgswap  25849  ply1divex  26134  plyeq0lem  26206  plymullem1  26210  dgrcolem1  26270  dgrcolem2  26271  vieta1lem2  26308  elqaalem2  26317  elqaalem3  26318  aaliou3lem7  26346  ulmshft  26388  mulcxplem  26680  cxpmul2  26685  root1eq1  26752  cxpeq  26754  logbchbase  26768  cosangneg2d  26804  isosctrlem2  26816  angpieqvdlem  26825  chordthmlem3  26831  chordthmlem4  26832  chordthmlem5  26833  quad2  26836  dcubic2  26841  cubic2  26845  quart1  26853  scvxcvx  26983  igamlgam  27047  lgam1  27061  basellem9  27086  ppifl  27157  mumul  27178  sgmmul  27199  chtublem  27209  chpub  27218  logfacrlim  27222  dchrsum2  27266  sumdchr2  27268  bposlem9  27290  lgsdir2  27328  lgsdir  27330  lgsdi  27332  lgsdirnn0  27342  lgsdinn0  27343  lgsquad3  27385  2sqblem  27429  chpo1ub  27478  dchrmusum2  27492  dchrvmasumlem1  27493  dchrvmasum2if  27495  dchrisum0fmul  27504  rpvmasum2  27510  mulog2sumlem1  27532  vmalogdivsum2  27536  log2sumbnd  27542  selberg3lem1  27555  selberg4lem1  27558  pntrsumo1  27563  selbergr  27566  pntpbnd1  27584  pntlemk  27604  mulsunif2lem  28139  divsasswd  28172  absmuls  28208  tgbtwnconn1lem3  28470  mideulem2  28630  axlowdimlem16  28860  axcontlem8  28874  vtxval  28905  iedgval  28906  edgval  28954  vtxdgop  29376  finsumvtxdg2size  29456  lp1cycl  30054  ex-ind-dvds  30363  vsfval  30535  lnocoi  30659  nmblolbii  30701  ipasslem5  30737  hvsubid  30928  sshjval3  31256  pjhthlem1  31293  adjval  31792  unopf1o  31818  kbpj  31858  lnopmi  31902  nmcoplbi  31930  cnlnadjlem2  31970  adjadd  31995  branmfn  32007  pjtoi  32081  ofoprabco  32551  supppreima  32573  hashxpe  32679  ccatws1f1o  32782  splfv3  32789  xrsmulgzz  32846  psgnfzto1stlem  32934  cycpmco2lem5  32964  cycpmco2lem6  32965  cyc3co2  32974  tocyccntz  32978  cyc3genpmlem  32985  cyc3conja  32991  archiabllem1a  33012  gsumvsca1  33046  gsumvsca2  33047  rloccring  33081  imaslmod  33185  elrspunidl  33261  mxidlirredi  33304  opprabs  33315  qsdrngi  33328  1arithidomlem1  33368  1arithidomlem2  33369  zringfrac  33387  ply1degltdimlem  33470  fedgmullem1  33477  algextdeglem4  33538  submat1n  33557  submatres  33558  madjusmdetlem3  33581  xrge0iifhom  33689  qqhval2lem  33733  qqhrhm  33741  qqhucn  33744  esumsnf  33834  measvunilem0  33983  carsgclctunlem1  34088  ballotlemfp1  34262  ballotlemsf1o  34284  signstfveq0  34360  breprexplemc  34415  breprexp  34416  breprexpnat  34417  circlemeth  34423  logdivsqrle  34433  hgt750lema  34440  revwlk  34885  cvmlift3lem2  35081  cvmlift3lem4  35083  cvmlift3lem5  35084  cvmlift3lem6  35085  cvmlift3lem9  35088  elmrsubrn  35281  bccolsum  35484  bj-bary1lem  36940  finixpnum  37229  poimirlem4  37248  poimirlem16  37260  poimirlem19  37263  poimirlem25  37269  mblfinlem3  37283  dvtan  37294  itg2addnc  37298  itgaddnclem2  37303  ftc1anclem6  37322  areacirclem5  37336  areacirc  37337  upixp  37353  prdsbnd2  37419  ismrer1  37462  rngoneglmul  37567  rngoisocnv  37605  islshpsm  38602  lshpnel2N  38607  lfl0f  38691  ldualvsdi1  38765  ldualgrplem  38767  cmtcomlemN  38870  cvlsupr8  38971  pmodl42N  39474  pmapjat1  39476  llnmod2i2  39486  dalawlem2  39495  pmapj2N  39552  idltrn  39773  cdlemc6  39819  cdleme20d  39935  cdleme22e  39967  cdleme22eALTN  39968  cdleme35b  40073  cdleme48fvg  40123  cdlemg4d  40236  cdlemg8a  40250  cdlemg42  40352  cdlemg47a  40357  tendodi1  40407  tendodi2  40408  cdlemk4  40457  cdlemk21N  40496  cdlemk22  40516  cdlemky  40549  cdlemk53b  40579  cdlemk53  40580  cdlemkyyN  40585  erngdvlem3-rN  40621  tendocnv  40644  dia1dim2  40685  dicvaddcl  40813  dihglblem3N  40918  dihmeetlem4preN  40929  dihmeet2  40969  lcfl7lem  41122  baerlem3lem1  41330  baerlem5alem1  41331  mapdh6bN  41360  mapdh6cN  41361  mapdh6dN  41362  hdmap1l6b  41434  hdmap1l6c  41435  hdmap1l6d  41436  hdmap14lem13  41503  ofun  41879  grpcominv1  41905  evlselv  41974  flt4lem7  42223  3cubeslem2  42252  3cubeslem3r  42254  3cubeslem4  42256  pellexlem2  42397  rmxyneg  42488  oddcomabszz  42512  acongeq  42551  hausgraph  42780  onsupnmax  42803  tfsconcatrev  42924  naddass1  42970  fsovrfovd  43586  inductionexd  43732  expgrowth  43919  binomcxplemwb  43932  binomcxplemnn0  43933  binomcxplemnotnn0  43940  sumsnd  44535  restuni4  44632  fmuldfeqlem1  45113  cncfmptss  45118  climexp  45136  dvresntr  45449  stoweidlem17  45548  wallispi  45601  dirkertrigeq  45632  dirkercncflem2  45635  fourierdlem30  45668  fourierdlem41  45679  fourierdlem81  45718  fourierdlem103  45740  sge0xp  45960  sge0isummpt2  45963  isomennd  46062  vonioolem1  46211  sigarperm  46391  fcores  46592  imasetpreimafvbijlemfo  46887  fundcmpsurbijinjpreimafv  46889  fundcmpsurinjimaid  46893  prprspr2  47000  opoeALTV  47165  cznrng  47514  rngchomrnghmresALTV  47532  fdmdifeqresdif  47596  lincsum  47688  lincscm  47689  lmod1lem4  47749  blennngt2o2  47856  blennn0e2  47858  topdlat  48206  reccot  48380  rectan  48381  cotsqcscsq  48384  amgmlemALT  48427