Theorem 3eqtr4rd 2781

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  csbun  4416  csbdif  4499  csbcnvgALT  5864  csbres  5969  fimacnvinrn2  7061  f1ossf1o  7117  suppvalbr  8161  odi  8589  phplem2  9217  cantnfp1lem3  9692  cantnfp1  9693  cardidm  9971  ackbij2lem2  10251  ackbij2lem3  10252  divneg  11931  xadddilem  13308  xadddi2  13311  dfceil2  13854  modlt  13895  modmulnn  13904  seqcaopr3  14053  bcval5  14334  hashgadd  14393  hashun3  14400  hashmap  14451  seqcoll  14480  revccat  14782  cshwmodn  14811  2cshwcom  14832  cshimadifsn0  14847  revco  14851  cshco  14853  ofccat  14986  relexpsucl  15048  dfrtrclrec2  15075  cjreb  15140  recj  15141  imcj  15149  imval2  15168  sqrtmul  15276  absmax  15346  amgm2  15386  summolem2a  15729  fsumf1o  15737  sumsnf  15757  sumsplit  15782  fsummulc2  15798  binom  15844  bcxmas  15849  incexclem  15850  incexc  15851  expcnv  15878  pwdif  15882  cvgrat  15897  prodmolem3  15947  prodmolem2a  15948  fprodf1o  15960  prodsn  15976  prodsnf  15978  fprodabs  15988  binomfallfac  16055  fallfacval4  16057  bcfallfac  16058  ege2le3  16104  efaddlem  16107  eftlub  16125  tanval3  16150  tanneg  16164  cosmul  16189  cos01bnd  16202  demoivreALT  16217  flodddiv4  16432  absmulgcd  16566  nn0expgcd  16581  lcmfunsnlem2  16657  eulerthlem2  16799  phisum  16808  pythagtriplem14  16846  pythagtriplem19  16851  pcmul  16869  pcfac  16917  prmreclem6  16939  4sqlem12  16974  vdwlem6  17004  oppccatid  17729  curf2ndf  18257  oppcyon  18279  joincomALT  18409  meetcomALT  18411  pwsco1mhm  18808  sgrp2nmndlem4  18904  qusgrp2  19039  mulgnngsum  19060  mulgnn0p1  19066  mulgneg  19073  mulgnn0dir  19085  qusghm  19236  gaid  19280  symgval  19350  pmtrdifellem3  19457  psgnunilem2  19474  odmulg  19535  sylow1lem2  19578  sylow2a  19598  sylow3lem1  19606  efgredleme  19722  efgcpbllemb  19734  gsumzaddlem  19900  gsumconst  19913  gsumzmhm  19916  ablsimpgfindlem1  20088  srgpcomp  20176  srgbinom  20189  rdivmuldivd  20371  c0mgm  20417  c0mhm  20418  zrrnghm  20494  imadrhmcl  20755  lmodvsmmulgdi  20852  lmodsubdi  20874  rmodislmodlem  20884  0lmhm  20996  lspsneq  21081  qusrhm  21235  quscrng  21242  zringlpirlem3  21423  mulgrhm  21436  phssip  21616  frlmip  21736  frlmphl  21739  asclmulg  21860  resspsrmul  21934  evlsscasrng  22053  psdadd  22099  psdvsca  22100  psdmul  22102  psdpw  22106  psropprmul  22171  evls1scasrng  22275  mat1ghm  22419  mat1mhm  22420  1marepvmarrepid  22511  mdetrlin  22538  mdetrsca2  22540  mdetunilem7  22554  mdetunilem9  22556  mndifsplit  22572  maducoeval2  22576  smadiadetglem2  22608  decpmatmul  22708  pm2mpghm  22752  pm2mpmhmlem2  22755  cpmidgsum2  22815  ptbasfi  23517  ptuni  23530  alexsubALTlem3  23985  subgtgp  24041  tsmsxplem1  24089  xmsusp  24506  restmetu  24507  nminv  24558  nrginvrcnlem  24628  copco  24967  pcoass  24973  pi1bas  24987  pi1xfrf  25002  pi1xfr  25004  isclmp  25046  cph2subdi  25160  cphassr  25162  tcphcphlem1  25185  cphipval  25193  rrxip  25340  rrxnm  25341  pjthlem1  25387  ovolunlem1a  25447  ovolfs2  25522  uniiccdif  25529  ismbf  25579  itgaddlem2  25775  ditgswap  25810  ply1divex  26092  plyeq0lem  26165  plymullem1  26169  dgrcolem1  26229  dgrcolem2  26230  vieta1lem2  26269  elqaalem2  26278  elqaalem3  26279  aaliou3lem7  26307  ulmshft  26349  mulcxplem  26643  cxpmul2  26648  root1eq1  26715  cxpeq  26717  logbchbase  26731  cosangneg2d  26767  isosctrlem2  26779  angpieqvdlem  26788  chordthmlem3  26794  chordthmlem4  26795  chordthmlem5  26796  quad2  26799  dcubic2  26804  cubic2  26808  quart1  26816  scvxcvx  26946  igamlgam  27010  lgam1  27024  basellem9  27049  ppifl  27120  mumul  27141  sgmmul  27162  chtublem  27172  chpub  27181  logfacrlim  27185  dchrsum2  27229  sumdchr2  27231  bposlem9  27253  lgsdir2  27291  lgsdir  27293  lgsdi  27295  lgsdirnn0  27305  lgsdinn0  27306  lgsquad3  27348  2sqblem  27392  chpo1ub  27441  dchrmusum2  27455  dchrvmasumlem1  27456  dchrvmasum2if  27458  dchrisum0fmul  27467  rpvmasum2  27473  mulog2sumlem1  27495  vmalogdivsum2  27499  log2sumbnd  27505  selberg3lem1  27518  selberg4lem1  27521  pntrsumo1  27526  selbergr  27529  pntpbnd1  27547  pntlemk  27567  mulsunif2lem  28112  divsasswd  28145  absmuls  28185  zscut  28310  expsp1  28329  tgbtwnconn1lem3  28499  mideulem2  28659  axlowdimlem16  28882  axcontlem8  28896  vtxval  28925  iedgval  28926  edgval  28974  vtxdgop  29396  finsumvtxdg2size  29476  lp1cycl  30079  ex-ind-dvds  30388  vsfval  30560  lnocoi  30684  nmblolbii  30726  ipasslem5  30762  hvsubid  30953  sshjval3  31281  pjhthlem1  31318  adjval  31817  unopf1o  31843  kbpj  31883  lnopmi  31927  nmcoplbi  31955  cnlnadjlem2  31995  adjadd  32020  branmfn  32032  pjtoi  32106  ofoprabco  32588  supppreima  32614  sgnval2  32658  hashxpe  32732  ccatws1f1o  32873  splfv3  32880  xrsmulgzz  32947  mndractfo  32970  mndlactf1o  32971  mndractf1o  32972  gsumfs2d  32995  psgnfzto1stlem  33057  cycpmco2lem5  33087  cycpmco2lem6  33088  cyc3co2  33097  tocyccntz  33101  cyc3genpmlem  33108  cyc3conja  33114  archiabllem1a  33135  gsumvsca1  33169  gsumvsca2  33170  elrgspnlem2  33184  elrgspnsubrunlem1  33188  rloccring  33211  imaslmod  33314  elrspunidl  33389  mxidlirredi  33432  opprabs  33443  qsdrngi  33456  1arithidomlem1  33496  1arithidomlem2  33497  zringfrac  33515  ressply1evls1  33524  ply1degltdimlem  33608  fedgmullem1  33615  fldextrspunlsplem  33660  algextdeglem4  33700  constrconj  33725  constrdircl  33745  constrremulcl  33747  constrimcl  33750  constrresqrtcl  33757  cos9thpiminplylem2  33763  submat1n  33782  submatres  33783  madjusmdetlem3  33806  xrge0iifhom  33914  qqhval2lem  33958  qqhrhm  33966  qqhucn  33969  esumsnf  34041  measvunilem0  34190  carsgclctunlem1  34295  ballotlemfp1  34470  ballotlemsf1o  34492  signstfveq0  34555  breprexplemc  34610  breprexp  34611  breprexpnat  34612  circlemeth  34618  logdivsqrle  34628  hgt750lema  34635  revwlk  35093  cvmlift3lem2  35288  cvmlift3lem4  35290  cvmlift3lem5  35291  cvmlift3lem6  35292  cvmlift3lem9  35295  elmrsubrn  35488  bccolsum  35702  bj-bary1lem  37274  finixpnum  37575  poimirlem4  37594  poimirlem16  37606  poimirlem19  37609  poimirlem25  37615  mblfinlem3  37629  dvtan  37640  itg2addnc  37644  itgaddnclem2  37649  ftc1anclem6  37668  areacirclem5  37682  areacirc  37683  upixp  37699  prdsbnd2  37765  ismrer1  37808  rngoneglmul  37913  rngoisocnv  37951  islshpsm  38944  lshpnel2N  38949  lfl0f  39033  ldualvsdi1  39107  ldualgrplem  39109  cmtcomlemN  39212  cvlsupr8  39313  pmodl42N  39816  pmapjat1  39818  llnmod2i2  39828  dalawlem2  39837  pmapj2N  39894  idltrn  40115  cdlemc6  40161  cdleme20d  40277  cdleme22e  40309  cdleme22eALTN  40310  cdleme35b  40415  cdleme48fvg  40465  cdlemg4d  40578  cdlemg8a  40592  cdlemg42  40694  cdlemg47a  40699  tendodi1  40749  tendodi2  40750  cdlemk4  40799  cdlemk21N  40838  cdlemk22  40858  cdlemky  40891  cdlemk53b  40921  cdlemk53  40922  cdlemkyyN  40927  erngdvlem3-rN  40963  tendocnv  40986  dia1dim2  41027  dicvaddcl  41155  dihglblem3N  41260  dihmeetlem4preN  41271  dihmeet2  41311  lcfl7lem  41464  baerlem3lem1  41672  baerlem5alem1  41673  mapdh6bN  41702  mapdh6cN  41703  mapdh6dN  41704  hdmap1l6b  41776  hdmap1l6c  41777  hdmap1l6d  41778  hdmap14lem13  41845  ofun  42234  grpcominv1  42478  evlselv  42557  flt4lem7  42629  3cubeslem2  42655  3cubeslem3r  42657  3cubeslem4  42659  pellexlem2  42800  rmxyneg  42891  oddcomabszz  42915  acongeq  42954  hausgraph  43176  onsupnmax  43199  tfsconcatrev  43319  naddass1  43364  fsovrfovd  43980  inductionexd  44126  expgrowth  44307  binomcxplemwb  44320  binomcxplemnn0  44321  binomcxplemnotnn0  44328  sumsnd  44998  restuni4  45093  fmuldfeqlem1  45559  cncfmptss  45564  climexp  45582  dvresntr  45895  stoweidlem17  45994  wallispi  46047  dirkertrigeq  46078  dirkercncflem2  46081  fourierdlem30  46114  fourierdlem41  46125  fourierdlem81  46164  fourierdlem103  46186  sge0xp  46406  sge0isummpt2  46409  isomennd  46508  vonioolem1  46657  sigarperm  46837  fcores  47044  imasetpreimafvbijlemfo  47367  fundcmpsurbijinjpreimafv  47369  fundcmpsurinjimaid  47373  prprspr2  47480  opoeALTV  47645  uhgrimisgrgric  47892  isubgr3stgrlem2  47927  cznrng  48184  rngchomrnghmresALTV  48202  fdmdifeqresdif  48265  lincsum  48353  lincscm  48354  lmod1lem4  48414  blennngt2o2  48520  blennn0e2  48522  tposideq  48811  topdlat  48926  sectpropdlem  48951  invpropdlem  48953  isopropdlem  48955  imaidfu  49017  imasubc  49039  swapfid  49144  swapfcoa  49146  diag1f1olem  49366  oppgoppchom  49415  oppgoppcco  49416  oppgoppcid  49417  2arwcat  49425  reccot  49570  rectan  49571  cotsqcscsq  49574  amgmlemALT  49615