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  4400  csbdif  4483  csbcnvgALT  5838  csbres  5942  fimacnvinrn2  7026  f1ossf1o  7082  suppvalbr  8120  odi  8520  phplem2  9146  cantnfp1lem3  9609  cantnfp1  9610  cardidm  9888  ackbij2lem2  10168  ackbij2lem3  10169  divneg  11850  xadddilem  13230  xadddi2  13233  dfceil2  13777  modlt  13818  modmulnn  13827  seqcaopr3  13978  bcval5  14259  hashgadd  14318  hashun3  14325  hashmap  14376  seqcoll  14405  revccat  14707  cshwmodn  14736  2cshwcom  14757  cshimadifsn0  14772  revco  14776  cshco  14778  ofccat  14911  relexpsucl  14973  dfrtrclrec2  15000  cjreb  15065  recj  15066  imcj  15074  imval2  15093  sqrtmul  15201  absmax  15272  amgm2  15312  summolem2a  15657  fsumf1o  15665  sumsnf  15685  sumsplit  15710  fsummulc2  15726  binom  15772  bcxmas  15777  incexclem  15778  incexc  15779  expcnv  15806  pwdif  15810  cvgrat  15825  prodmolem3  15875  prodmolem2a  15876  fprodf1o  15888  prodsn  15904  prodsnf  15906  fprodabs  15916  binomfallfac  15983  fallfacval4  15985  bcfallfac  15986  ege2le3  16032  efaddlem  16035  eftlub  16053  tanval3  16078  tanneg  16092  cosmul  16117  cos01bnd  16130  demoivreALT  16145  flodddiv4  16361  absmulgcd  16495  nn0expgcd  16510  lcmfunsnlem2  16586  eulerthlem2  16728  phisum  16737  pythagtriplem14  16775  pythagtriplem19  16780  pcmul  16798  pcfac  16846  prmreclem6  16868  4sqlem12  16903  vdwlem6  16933  oppccatid  17660  curf2ndf  18188  oppcyon  18210  joincomALT  18340  meetcomALT  18342  pwsco1mhm  18741  sgrp2nmndlem4  18837  qusgrp2  18972  mulgnngsum  18993  mulgnn0p1  18999  mulgneg  19006  mulgnn0dir  19018  qusghm  19169  gaid  19213  symgval  19285  pmtrdifellem3  19392  psgnunilem2  19409  odmulg  19470  sylow1lem2  19513  sylow2a  19533  sylow3lem1  19541  efgredleme  19657  efgcpbllemb  19669  gsumzaddlem  19835  gsumconst  19848  gsumzmhm  19851  ablsimpgfindlem1  20023  srgpcomp  20138  srgbinom  20151  rdivmuldivd  20333  c0mgm  20379  c0mhm  20380  zrrnghm  20456  imadrhmcl  20717  lmodvsmmulgdi  20835  lmodsubdi  20857  rmodislmodlem  20867  0lmhm  20979  lspsneq  21064  qusrhm  21218  quscrng  21225  zringlpirlem3  21406  mulgrhm  21419  phssip  21600  frlmip  21720  frlmphl  21723  asclmulg  21844  resspsrmul  21918  evlsscasrng  22037  psdadd  22083  psdvsca  22084  psdmul  22086  psdpw  22090  psropprmul  22155  evls1scasrng  22259  mat1ghm  22403  mat1mhm  22404  1marepvmarrepid  22495  mdetrlin  22522  mdetrsca2  22524  mdetunilem7  22538  mdetunilem9  22540  mndifsplit  22556  maducoeval2  22560  smadiadetglem2  22592  decpmatmul  22692  pm2mpghm  22736  pm2mpmhmlem2  22739  cpmidgsum2  22799  ptbasfi  23501  ptuni  23514  alexsubALTlem3  23969  subgtgp  24025  tsmsxplem1  24073  xmsusp  24490  restmetu  24491  nminv  24542  nrginvrcnlem  24612  copco  24951  pcoass  24957  pi1bas  24971  pi1xfrf  24986  pi1xfr  24988  isclmp  25030  cph2subdi  25143  cphassr  25145  tcphcphlem1  25168  cphipval  25176  rrxip  25323  rrxnm  25324  pjthlem1  25370  ovolunlem1a  25430  ovolfs2  25505  uniiccdif  25512  ismbf  25562  itgaddlem2  25758  ditgswap  25793  ply1divex  26075  plyeq0lem  26148  plymullem1  26152  dgrcolem1  26212  dgrcolem2  26213  vieta1lem2  26252  elqaalem2  26261  elqaalem3  26262  aaliou3lem7  26290  ulmshft  26332  mulcxplem  26626  cxpmul2  26631  root1eq1  26698  cxpeq  26700  logbchbase  26714  cosangneg2d  26750  isosctrlem2  26762  angpieqvdlem  26771  chordthmlem3  26777  chordthmlem4  26778  chordthmlem5  26779  quad2  26782  dcubic2  26787  cubic2  26791  quart1  26799  scvxcvx  26929  igamlgam  26993  lgam1  27007  basellem9  27032  ppifl  27103  mumul  27124  sgmmul  27145  chtublem  27155  chpub  27164  logfacrlim  27168  dchrsum2  27212  sumdchr2  27214  bposlem9  27236  lgsdir2  27274  lgsdir  27276  lgsdi  27278  lgsdirnn0  27288  lgsdinn0  27289  lgsquad3  27331  2sqblem  27375  chpo1ub  27424  dchrmusum2  27438  dchrvmasumlem1  27439  dchrvmasum2if  27441  dchrisum0fmul  27450  rpvmasum2  27456  mulog2sumlem1  27478  vmalogdivsum2  27482  log2sumbnd  27488  selberg3lem1  27501  selberg4lem1  27504  pntrsumo1  27509  selbergr  27512  pntpbnd1  27530  pntlemk  27550  mulsunif2lem  28112  divsasswd  28146  absmuls  28186  eucliddivs  28305  zscut  28335  expsp1  28356  expadds  28362  pw2divsrecd  28374  tgbtwnconn1lem3  28554  mideulem2  28714  axlowdimlem16  28937  axcontlem8  28951  vtxval  28980  iedgval  28981  edgval  29029  vtxdgop  29451  finsumvtxdg2size  29531  lp1cycl  30131  ex-ind-dvds  30440  vsfval  30612  lnocoi  30736  nmblolbii  30778  ipasslem5  30814  hvsubid  31005  sshjval3  31333  pjhthlem1  31370  adjval  31869  unopf1o  31895  kbpj  31935  lnopmi  31979  nmcoplbi  32007  cnlnadjlem2  32047  adjadd  32072  branmfn  32084  pjtoi  32158  ofoprabco  32638  supppreima  32664  sgnval2  32708  hashxpe  32782  ccatws1f1o  32923  splfv3  32930  xrsmulgzz  32993  mndractfo  33013  mndlactf1o  33014  mndractf1o  33015  gsumfs2d  33038  psgnfzto1stlem  33072  cycpmco2lem5  33102  cycpmco2lem6  33103  cyc3co2  33112  tocyccntz  33116  cyc3genpmlem  33123  cyc3conja  33129  archiabllem1a  33160  gsumvsca1  33195  gsumvsca2  33196  elrgspnlem2  33210  elrgspnsubrunlem1  33214  rloccring  33237  imaslmod  33317  elrspunidl  33392  mxidlirredi  33435  opprabs  33446  qsdrngi  33459  1arithidomlem1  33499  1arithidomlem2  33500  zringfrac  33518  ressply1evls1  33527  ply1degltdimlem  33611  fedgmullem1  33618  fldextrspunlsplem  33661  algextdeglem4  33703  constrconj  33728  constrdircl  33748  constrremulcl  33750  constrimcl  33753  constrresqrtcl  33760  cos9thpiminplylem2  33766  submat1n  33788  submatres  33789  madjusmdetlem3  33812  xrge0iifhom  33920  qqhval2lem  33964  qqhrhm  33972  qqhucn  33975  esumsnf  34047  measvunilem0  34196  carsgclctunlem1  34301  ballotlemfp1  34476  ballotlemsf1o  34498  signstfveq0  34561  breprexplemc  34616  breprexp  34617  breprexpnat  34618  circlemeth  34624  logdivsqrle  34634  hgt750lema  34641  revwlk  35105  cvmlift3lem2  35300  cvmlift3lem4  35302  cvmlift3lem5  35303  cvmlift3lem6  35304  cvmlift3lem9  35307  elmrsubrn  35500  bccolsum  35719  bj-bary1lem  37291  finixpnum  37592  poimirlem4  37611  poimirlem16  37623  poimirlem19  37626  poimirlem25  37632  mblfinlem3  37646  dvtan  37657  itg2addnc  37661  itgaddnclem2  37666  ftc1anclem6  37685  areacirclem5  37699  areacirc  37700  upixp  37716  prdsbnd2  37782  ismrer1  37825  rngoneglmul  37930  rngoisocnv  37968  islshpsm  38966  lshpnel2N  38971  lfl0f  39055  ldualvsdi1  39129  ldualgrplem  39131  cmtcomlemN  39234  cvlsupr8  39335  pmodl42N  39838  pmapjat1  39840  llnmod2i2  39850  dalawlem2  39859  pmapj2N  39916  idltrn  40137  cdlemc6  40183  cdleme20d  40299  cdleme22e  40331  cdleme22eALTN  40332  cdleme35b  40437  cdleme48fvg  40487  cdlemg4d  40600  cdlemg8a  40614  cdlemg42  40716  cdlemg47a  40721  tendodi1  40771  tendodi2  40772  cdlemk4  40821  cdlemk21N  40860  cdlemk22  40880  cdlemky  40913  cdlemk53b  40943  cdlemk53  40944  cdlemkyyN  40949  erngdvlem3-rN  40985  tendocnv  41008  dia1dim2  41049  dicvaddcl  41177  dihglblem3N  41282  dihmeetlem4preN  41293  dihmeet2  41333  lcfl7lem  41486  baerlem3lem1  41694  baerlem5alem1  41695  mapdh6bN  41724  mapdh6cN  41725  mapdh6dN  41726  hdmap1l6b  41798  hdmap1l6c  41799  hdmap1l6d  41800  hdmap14lem13  41867  ofun  42217  grpcominv1  42489  evlselv  42568  flt4lem7  42640  3cubeslem2  42666  3cubeslem3r  42668  3cubeslem4  42670  pellexlem2  42811  rmxyneg  42902  oddcomabszz  42926  acongeq  42965  hausgraph  43187  onsupnmax  43210  tfsconcatrev  43330  naddass1  43375  fsovrfovd  43991  inductionexd  44137  expgrowth  44317  binomcxplemwb  44330  binomcxplemnn0  44331  binomcxplemnotnn0  44338  sumsnd  45013  restuni4  45108  fmuldfeqlem1  45573  cncfmptss  45578  climexp  45596  dvresntr  45909  stoweidlem17  46008  wallispi  46061  dirkertrigeq  46092  dirkercncflem2  46095  fourierdlem30  46128  fourierdlem41  46139  fourierdlem81  46178  fourierdlem103  46200  sge0xp  46420  sge0isummpt2  46423  isomennd  46522  vonioolem1  46671  sigarperm  46851  fcores  47061  imasetpreimafvbijlemfo  47399  fundcmpsurbijinjpreimafv  47401  fundcmpsurinjimaid  47405  prprspr2  47512  opoeALTV  47677  uhgrimisgrgric  47924  isubgr3stgrlem2  47959  cznrng  48242  rngchomrnghmresALTV  48260  fdmdifeqresdif  48323  lincsum  48411  lincscm  48412  lmod1lem4  48472  blennngt2o2  48574  blennn0e2  48576  tposideq  48869  topdlat  48985  sectpropdlem  49018  invpropdlem  49020  isopropdlem  49022  imaidfu  49092  imasubc  49133  natoppf  49211  swapfid  49261  swapfcoa  49263  fucoppcid  49390  fucoppcco  49391  oppfdiag1  49396  diag1f1olem  49515  oppgoppchom  49572  oppgoppcco  49573  oppgoppcid  49574  2arwcat  49582  reccot  49740  rectan  49741  cotsqcscsq  49744  amgmlemALT  49785