Theorem 3eqtr4rd 2775

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 2767	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
4		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
5	3, 4	eqtr4d 2767	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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  csbun  4404  csbdif  4487  csbcnvgALT  5848  csbres  5953  fimacnvinrn2  7044  f1ossf1o  7100  suppvalbr  8143  odi  8543  phplem2  9169  cantnfp1lem3  9633  cantnfp1  9634  cardidm  9912  ackbij2lem2  10192  ackbij2lem3  10193  divneg  11874  xadddilem  13254  xadddi2  13257  dfceil2  13801  modlt  13842  modmulnn  13851  seqcaopr3  14002  bcval5  14283  hashgadd  14342  hashun3  14349  hashmap  14400  seqcoll  14429  revccat  14731  cshwmodn  14760  2cshwcom  14781  cshimadifsn0  14796  revco  14800  cshco  14802  ofccat  14935  relexpsucl  14997  dfrtrclrec2  15024  cjreb  15089  recj  15090  imcj  15098  imval2  15117  sqrtmul  15225  absmax  15296  amgm2  15336  summolem2a  15681  fsumf1o  15689  sumsnf  15709  sumsplit  15734  fsummulc2  15750  binom  15796  bcxmas  15801  incexclem  15802  incexc  15803  expcnv  15830  pwdif  15834  cvgrat  15849  prodmolem3  15899  prodmolem2a  15900  fprodf1o  15912  prodsn  15928  prodsnf  15930  fprodabs  15940  binomfallfac  16007  fallfacval4  16009  bcfallfac  16010  ege2le3  16056  efaddlem  16059  eftlub  16077  tanval3  16102  tanneg  16116  cosmul  16141  cos01bnd  16154  demoivreALT  16169  flodddiv4  16385  absmulgcd  16519  nn0expgcd  16534  lcmfunsnlem2  16610  eulerthlem2  16752  phisum  16761  pythagtriplem14  16799  pythagtriplem19  16804  pcmul  16822  pcfac  16870  prmreclem6  16892  4sqlem12  16927  vdwlem6  16957  oppccatid  17680  curf2ndf  18208  oppcyon  18230  joincomALT  18360  meetcomALT  18362  pwsco1mhm  18759  sgrp2nmndlem4  18855  qusgrp2  18990  mulgnngsum  19011  mulgnn0p1  19017  mulgneg  19024  mulgnn0dir  19036  qusghm  19187  gaid  19231  symgval  19301  pmtrdifellem3  19408  psgnunilem2  19425  odmulg  19486  sylow1lem2  19529  sylow2a  19549  sylow3lem1  19557  efgredleme  19673  efgcpbllemb  19685  gsumzaddlem  19851  gsumconst  19864  gsumzmhm  19867  ablsimpgfindlem1  20039  srgpcomp  20127  srgbinom  20140  rdivmuldivd  20322  c0mgm  20368  c0mhm  20369  zrrnghm  20445  imadrhmcl  20706  lmodvsmmulgdi  20803  lmodsubdi  20825  rmodislmodlem  20835  0lmhm  20947  lspsneq  21032  qusrhm  21186  quscrng  21193  zringlpirlem3  21374  mulgrhm  21387  phssip  21567  frlmip  21687  frlmphl  21690  asclmulg  21811  resspsrmul  21885  evlsscasrng  22004  psdadd  22050  psdvsca  22051  psdmul  22053  psdpw  22057  psropprmul  22122  evls1scasrng  22226  mat1ghm  22370  mat1mhm  22371  1marepvmarrepid  22462  mdetrlin  22489  mdetrsca2  22491  mdetunilem7  22505  mdetunilem9  22507  mndifsplit  22523  maducoeval2  22527  smadiadetglem2  22559  decpmatmul  22659  pm2mpghm  22703  pm2mpmhmlem2  22706  cpmidgsum2  22766  ptbasfi  23468  ptuni  23481  alexsubALTlem3  23936  subgtgp  23992  tsmsxplem1  24040  xmsusp  24457  restmetu  24458  nminv  24509  nrginvrcnlem  24579  copco  24918  pcoass  24924  pi1bas  24938  pi1xfrf  24953  pi1xfr  24955  isclmp  24997  cph2subdi  25110  cphassr  25112  tcphcphlem1  25135  cphipval  25143  rrxip  25290  rrxnm  25291  pjthlem1  25337  ovolunlem1a  25397  ovolfs2  25472  uniiccdif  25479  ismbf  25529  itgaddlem2  25725  ditgswap  25760  ply1divex  26042  plyeq0lem  26115  plymullem1  26119  dgrcolem1  26179  dgrcolem2  26180  vieta1lem2  26219  elqaalem2  26228  elqaalem3  26229  aaliou3lem7  26257  ulmshft  26299  mulcxplem  26593  cxpmul2  26598  root1eq1  26665  cxpeq  26667  logbchbase  26681  cosangneg2d  26717  isosctrlem2  26729  angpieqvdlem  26738  chordthmlem3  26744  chordthmlem4  26745  chordthmlem5  26746  quad2  26749  dcubic2  26754  cubic2  26758  quart1  26766  scvxcvx  26896  igamlgam  26960  lgam1  26974  basellem9  26999  ppifl  27070  mumul  27091  sgmmul  27112  chtublem  27122  chpub  27131  logfacrlim  27135  dchrsum2  27179  sumdchr2  27181  bposlem9  27203  lgsdir2  27241  lgsdir  27243  lgsdi  27245  lgsdirnn0  27255  lgsdinn0  27256  lgsquad3  27298  2sqblem  27342  chpo1ub  27391  dchrmusum2  27405  dchrvmasumlem1  27406  dchrvmasum2if  27408  dchrisum0fmul  27417  rpvmasum2  27423  mulog2sumlem1  27445  vmalogdivsum2  27449  log2sumbnd  27455  selberg3lem1  27468  selberg4lem1  27471  pntrsumo1  27476  selbergr  27479  pntpbnd1  27497  pntlemk  27517  mulsunif2lem  28072  divsasswd  28106  absmuls  28146  eucliddivs  28265  zscut  28295  expsp1  28315  expadds  28320  pw2divsrecd  28330  tgbtwnconn1lem3  28501  mideulem2  28661  axlowdimlem16  28884  axcontlem8  28898  vtxval  28927  iedgval  28928  edgval  28976  vtxdgop  29398  finsumvtxdg2size  29478  lp1cycl  30081  ex-ind-dvds  30390  vsfval  30562  lnocoi  30686  nmblolbii  30728  ipasslem5  30764  hvsubid  30955  sshjval3  31283  pjhthlem1  31320  adjval  31819  unopf1o  31845  kbpj  31885  lnopmi  31929  nmcoplbi  31957  cnlnadjlem2  31997  adjadd  32022  branmfn  32034  pjtoi  32108  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  33145  gsumvsca1  33179  gsumvsca2  33180  elrgspnlem2  33194  elrgspnsubrunlem1  33198  rloccring  33221  imaslmod  33324  elrspunidl  33399  mxidlirredi  33442  opprabs  33453  qsdrngi  33466  1arithidomlem1  33506  1arithidomlem2  33507  zringfrac  33525  ressply1evls1  33534  ply1degltdimlem  33618  fedgmullem1  33625  fldextrspunlsplem  33668  algextdeglem4  33710  constrconj  33735  constrdircl  33755  constrremulcl  33757  constrimcl  33760  constrresqrtcl  33767  cos9thpiminplylem2  33773  submat1n  33795  submatres  33796  madjusmdetlem3  33819  xrge0iifhom  33927  qqhval2lem  33971  qqhrhm  33979  qqhucn  33982  esumsnf  34054  measvunilem0  34203  carsgclctunlem1  34308  ballotlemfp1  34483  ballotlemsf1o  34505  signstfveq0  34568  breprexplemc  34623  breprexp  34624  breprexpnat  34625  circlemeth  34631  logdivsqrle  34641  hgt750lema  34648  revwlk  35112  cvmlift3lem2  35307  cvmlift3lem4  35309  cvmlift3lem5  35310  cvmlift3lem6  35311  cvmlift3lem9  35314  elmrsubrn  35507  bccolsum  35726  bj-bary1lem  37298  finixpnum  37599  poimirlem4  37618  poimirlem16  37630  poimirlem19  37633  poimirlem25  37639  mblfinlem3  37653  dvtan  37664  itg2addnc  37668  itgaddnclem2  37673  ftc1anclem6  37692  areacirclem5  37706  areacirc  37707  upixp  37723  prdsbnd2  37789  ismrer1  37832  rngoneglmul  37937  rngoisocnv  37975  islshpsm  38973  lshpnel2N  38978  lfl0f  39062  ldualvsdi1  39136  ldualgrplem  39138  cmtcomlemN  39241  cvlsupr8  39342  pmodl42N  39845  pmapjat1  39847  llnmod2i2  39857  dalawlem2  39866  pmapj2N  39923  idltrn  40144  cdlemc6  40190  cdleme20d  40306  cdleme22e  40338  cdleme22eALTN  40339  cdleme35b  40444  cdleme48fvg  40494  cdlemg4d  40607  cdlemg8a  40621  cdlemg42  40723  cdlemg47a  40728  tendodi1  40778  tendodi2  40779  cdlemk4  40828  cdlemk21N  40867  cdlemk22  40887  cdlemky  40920  cdlemk53b  40950  cdlemk53  40951  cdlemkyyN  40956  erngdvlem3-rN  40992  tendocnv  41015  dia1dim2  41056  dicvaddcl  41184  dihglblem3N  41289  dihmeetlem4preN  41300  dihmeet2  41340  lcfl7lem  41493  baerlem3lem1  41701  baerlem5alem1  41702  mapdh6bN  41731  mapdh6cN  41732  mapdh6dN  41733  hdmap1l6b  41805  hdmap1l6c  41806  hdmap1l6d  41807  hdmap14lem13  41874  ofun  42224  grpcominv1  42496  evlselv  42575  flt4lem7  42647  3cubeslem2  42673  3cubeslem3r  42675  3cubeslem4  42677  pellexlem2  42818  rmxyneg  42909  oddcomabszz  42933  acongeq  42972  hausgraph  43194  onsupnmax  43217  tfsconcatrev  43337  naddass1  43382  fsovrfovd  43998  inductionexd  44144  expgrowth  44324  binomcxplemwb  44337  binomcxplemnn0  44338  binomcxplemnotnn0  44345  sumsnd  45020  restuni4  45115  fmuldfeqlem1  45580  cncfmptss  45585  climexp  45603  dvresntr  45916  stoweidlem17  46015  wallispi  46068  dirkertrigeq  46099  dirkercncflem2  46102  fourierdlem30  46135  fourierdlem41  46146  fourierdlem81  46185  fourierdlem103  46207  sge0xp  46427  sge0isummpt2  46430  isomennd  46529  vonioolem1  46678  sigarperm  46858  fcores  47068  imasetpreimafvbijlemfo  47406  fundcmpsurbijinjpreimafv  47408  fundcmpsurinjimaid  47412  prprspr2  47519  opoeALTV  47684  uhgrimisgrgric  47931  isubgr3stgrlem2  47966  cznrng  48249  rngchomrnghmresALTV  48267  fdmdifeqresdif  48330  lincsum  48418  lincscm  48419  lmod1lem4  48479  blennngt2o2  48581  blennn0e2  48583  tposideq  48876  topdlat  48992  sectpropdlem  49025  invpropdlem  49027  isopropdlem  49029  imaidfu  49099  imasubc  49140  natoppf  49218  swapfid  49268  swapfcoa  49270  fucoppcid  49397  fucoppcco  49398  oppfdiag1  49403  diag1f1olem  49522  oppgoppchom  49579  oppgoppcco  49580  oppgoppcid  49581  2arwcat  49589  reccot  49747  rectan  49748  cotsqcscsq  49751  amgmlemALT  49792