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  4392  csbdif  4475  csbcnvgALT  5827  csbres  5933  fimacnvinrn2  7006  f1ossf1o  7062  suppvalbr  8097  odi  8497  phplem2  9119  cantnfp1lem3  9576  cantnfp1  9577  cardidm  9855  ackbij2lem2  10133  ackbij2lem3  10134  divneg  11816  xadddilem  13196  xadddi2  13199  dfceil2  13743  modlt  13784  modmulnn  13793  seqcaopr3  13944  bcval5  14225  hashgadd  14284  hashun3  14291  hashmap  14342  seqcoll  14371  revccat  14672  cshwmodn  14701  2cshwcom  14722  cshimadifsn0  14737  revco  14741  cshco  14743  ofccat  14876  relexpsucl  14938  dfrtrclrec2  14965  cjreb  15030  recj  15031  imcj  15039  imval2  15058  sqrtmul  15166  absmax  15237  amgm2  15277  summolem2a  15622  fsumf1o  15630  sumsnf  15650  sumsplit  15675  fsummulc2  15691  binom  15737  bcxmas  15742  incexclem  15743  incexc  15744  expcnv  15771  pwdif  15775  cvgrat  15790  prodmolem3  15840  prodmolem2a  15841  fprodf1o  15853  prodsn  15869  prodsnf  15871  fprodabs  15881  binomfallfac  15948  fallfacval4  15950  bcfallfac  15951  ege2le3  15997  efaddlem  16000  eftlub  16018  tanval3  16043  tanneg  16057  cosmul  16082  cos01bnd  16095  demoivreALT  16110  flodddiv4  16326  absmulgcd  16460  nn0expgcd  16475  lcmfunsnlem2  16551  eulerthlem2  16693  phisum  16702  pythagtriplem14  16740  pythagtriplem19  16745  pcmul  16763  pcfac  16811  prmreclem6  16833  4sqlem12  16868  vdwlem6  16898  oppccatid  17625  curf2ndf  18153  oppcyon  18175  joincomALT  18305  meetcomALT  18307  pwsco1mhm  18706  sgrp2nmndlem4  18802  qusgrp2  18937  mulgnngsum  18958  mulgnn0p1  18964  mulgneg  18971  mulgnn0dir  18983  qusghm  19134  gaid  19178  symgval  19250  pmtrdifellem3  19357  psgnunilem2  19374  odmulg  19435  sylow1lem2  19478  sylow2a  19498  sylow3lem1  19506  efgredleme  19622  efgcpbllemb  19634  gsumzaddlem  19800  gsumconst  19813  gsumzmhm  19816  ablsimpgfindlem1  19988  srgpcomp  20103  srgbinom  20116  rdivmuldivd  20298  c0mgm  20344  c0mhm  20345  zrrnghm  20421  imadrhmcl  20682  lmodvsmmulgdi  20800  lmodsubdi  20822  rmodislmodlem  20832  0lmhm  20944  lspsneq  21029  qusrhm  21183  quscrng  21190  zringlpirlem3  21371  mulgrhm  21384  phssip  21565  frlmip  21685  frlmphl  21688  asclmulg  21809  resspsrmul  21883  evlsscasrng  22002  psdadd  22048  psdvsca  22049  psdmul  22051  psdpw  22055  psropprmul  22120  evls1scasrng  22224  mat1ghm  22368  mat1mhm  22369  1marepvmarrepid  22460  mdetrlin  22487  mdetrsca2  22489  mdetunilem7  22503  mdetunilem9  22505  mndifsplit  22521  maducoeval2  22525  smadiadetglem2  22557  decpmatmul  22657  pm2mpghm  22701  pm2mpmhmlem2  22704  cpmidgsum2  22764  ptbasfi  23466  ptuni  23479  alexsubALTlem3  23934  subgtgp  23990  tsmsxplem1  24038  xmsusp  24455  restmetu  24456  nminv  24507  nrginvrcnlem  24577  copco  24916  pcoass  24922  pi1bas  24936  pi1xfrf  24951  pi1xfr  24953  isclmp  24995  cph2subdi  25108  cphassr  25110  tcphcphlem1  25133  cphipval  25141  rrxip  25288  rrxnm  25289  pjthlem1  25335  ovolunlem1a  25395  ovolfs2  25470  uniiccdif  25477  ismbf  25527  itgaddlem2  25723  ditgswap  25758  ply1divex  26040  plyeq0lem  26113  plymullem1  26117  dgrcolem1  26177  dgrcolem2  26178  vieta1lem2  26217  elqaalem2  26226  elqaalem3  26227  aaliou3lem7  26255  ulmshft  26297  mulcxplem  26591  cxpmul2  26596  root1eq1  26663  cxpeq  26665  logbchbase  26679  cosangneg2d  26715  isosctrlem2  26727  angpieqvdlem  26736  chordthmlem3  26742  chordthmlem4  26743  chordthmlem5  26744  quad2  26747  dcubic2  26752  cubic2  26756  quart1  26764  scvxcvx  26894  igamlgam  26958  lgam1  26972  basellem9  26997  ppifl  27068  mumul  27089  sgmmul  27110  chtublem  27120  chpub  27129  logfacrlim  27133  dchrsum2  27177  sumdchr2  27179  bposlem9  27201  lgsdir2  27239  lgsdir  27241  lgsdi  27243  lgsdirnn0  27253  lgsdinn0  27254  lgsquad3  27296  2sqblem  27340  chpo1ub  27389  dchrmusum2  27403  dchrvmasumlem1  27404  dchrvmasum2if  27406  dchrisum0fmul  27415  rpvmasum2  27421  mulog2sumlem1  27443  vmalogdivsum2  27447  log2sumbnd  27453  selberg3lem1  27466  selberg4lem1  27469  pntrsumo1  27474  selbergr  27477  pntpbnd1  27495  pntlemk  27515  mulsunif2lem  28077  divsasswd  28111  absmuls  28151  eucliddivs  28270  zscut  28300  expsp1  28321  expadds  28327  pw2divsrecd  28339  tgbtwnconn1lem3  28519  mideulem2  28679  axlowdimlem16  28902  axcontlem8  28916  vtxval  28945  iedgval  28946  edgval  28994  vtxdgop  29416  finsumvtxdg2size  29496  lp1cycl  30096  ex-ind-dvds  30405  vsfval  30577  lnocoi  30701  nmblolbii  30743  ipasslem5  30779  hvsubid  30970  sshjval3  31298  pjhthlem1  31335  adjval  31834  unopf1o  31860  kbpj  31900  lnopmi  31944  nmcoplbi  31972  cnlnadjlem2  32012  adjadd  32037  branmfn  32049  pjtoi  32123  fconst7v  32565  ofoprabco  32608  supppreima  32634  sgnval2  32679  hashxpe  32753  ccatws1f1o  32894  splfv3  32901  xrsmulgzz  32964  mndractfo  32984  mndlactf1o  32985  mndractf1o  32986  gsumfs2d  33009  psgnfzto1stlem  33043  cycpmco2lem5  33073  cycpmco2lem6  33074  cyc3co2  33083  tocyccntz  33087  cyc3genpmlem  33094  cyc3conja  33100  archiabllem1a  33134  gsumvsca1  33169  gsumvsca2  33170  elrgspnlem2  33184  elrgspnsubrunlem1  33188  rloccring  33211  imaslmod  33291  elrspunidl  33366  mxidlirredi  33409  opprabs  33420  qsdrngi  33433  1arithidomlem1  33473  1arithidomlem2  33474  zringfrac  33492  ressply1evls1  33501  psrbasfsupp  33545  mplvrpmga  33548  ply1degltdimlem  33595  fedgmullem1  33602  fldextrspunlsplem  33646  extdgfialglem2  33666  algextdeglem4  33693  constrconj  33718  constrdircl  33738  constrremulcl  33740  constrimcl  33743  constrresqrtcl  33750  cos9thpiminplylem2  33756  submat1n  33778  submatres  33779  madjusmdetlem3  33802  xrge0iifhom  33910  qqhval2lem  33954  qqhrhm  33962  qqhucn  33965  esumsnf  34037  measvunilem0  34186  carsgclctunlem1  34291  ballotlemfp1  34466  ballotlemsf1o  34488  signstfveq0  34551  breprexplemc  34606  breprexp  34607  breprexpnat  34608  circlemeth  34614  logdivsqrle  34624  hgt750lema  34631  revwlk  35108  cvmlift3lem2  35303  cvmlift3lem4  35305  cvmlift3lem5  35306  cvmlift3lem6  35307  cvmlift3lem9  35310  elmrsubrn  35503  bccolsum  35722  bj-bary1lem  37294  finixpnum  37595  poimirlem4  37614  poimirlem16  37626  poimirlem19  37629  poimirlem25  37635  mblfinlem3  37649  dvtan  37660  itg2addnc  37664  itgaddnclem2  37669  ftc1anclem6  37688  areacirclem5  37702  areacirc  37703  upixp  37719  prdsbnd2  37785  ismrer1  37828  rngoneglmul  37933  rngoisocnv  37971  islshpsm  38969  lshpnel2N  38974  lfl0f  39058  ldualvsdi1  39132  ldualgrplem  39134  cmtcomlemN  39237  cvlsupr8  39338  pmodl42N  39840  pmapjat1  39842  llnmod2i2  39852  dalawlem2  39861  pmapj2N  39918  idltrn  40139  cdlemc6  40185  cdleme20d  40301  cdleme22e  40333  cdleme22eALTN  40334  cdleme35b  40439  cdleme48fvg  40489  cdlemg4d  40602  cdlemg8a  40616  cdlemg42  40718  cdlemg47a  40723  tendodi1  40773  tendodi2  40774  cdlemk4  40823  cdlemk21N  40862  cdlemk22  40882  cdlemky  40915  cdlemk53b  40945  cdlemk53  40946  cdlemkyyN  40951  erngdvlem3-rN  40987  tendocnv  41010  dia1dim2  41051  dicvaddcl  41179  dihglblem3N  41284  dihmeetlem4preN  41295  dihmeet2  41335  lcfl7lem  41488  baerlem3lem1  41696  baerlem5alem1  41697  mapdh6bN  41726  mapdh6cN  41727  mapdh6dN  41728  hdmap1l6b  41800  hdmap1l6c  41801  hdmap1l6d  41802  hdmap14lem13  41869  ofun  42219  grpcominv1  42491  evlselv  42570  flt4lem7  42642  3cubeslem2  42668  3cubeslem3r  42670  3cubeslem4  42672  pellexlem2  42813  rmxyneg  42903  oddcomabszz  42927  acongeq  42966  hausgraph  43188  onsupnmax  43211  tfsconcatrev  43331  naddass1  43376  fsovrfovd  43992  inductionexd  44138  expgrowth  44318  binomcxplemwb  44331  binomcxplemnn0  44332  binomcxplemnotnn0  44339  sumsnd  45014  restuni4  45109  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  47925  isubgr3stgrlem2  47961  cznrng  48255  rngchomrnghmresALTV  48273  fdmdifeqresdif  48336  lincsum  48424  lincscm  48425  lmod1lem4  48485  blennngt2o2  48587  blennn0e2  48589  tposideq  48882  topdlat  48998  sectpropdlem  49031  invpropdlem  49033  isopropdlem  49035  imaidfu  49105  imasubc  49146  natoppf  49224  swapfid  49274  swapfcoa  49276  fucoppcid  49403  fucoppcco  49404  oppfdiag1  49409  diag1f1olem  49528  oppgoppchom  49585  oppgoppcco  49586  oppgoppcid  49587  2arwcat  49595  reccot  49753  rectan  49754  cotsqcscsq  49757  amgmlemALT  49798