Theorem 3eqtr4rd 2815

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

Syntax hints:   → wi 4   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  csbun  4412  csbdif  4491  csbcnvgALTOLD  5875  csbres  5982  fimacnvinrn2  7068  f1ossf1o  7125  suppvalbr  8160  odi  8564  phplem2  9189  cantnfp1lem3  9649  cantnfp1  9650  cardidm  9945  ackbij2lem2  10222  ackbij2lem3  10223  divneg  11906  xadddilem  13320  xadddi2  13323  dfceil2  13872  modlt  13913  modmulnn  13922  seqcaopr3  14073  bcval5  14354  hashgadd  14413  hashun3  14420  hashmap  14472  seqcoll  14501  revccat  14803  cshwmodn  14832  2cshwcom  14853  cshimadifsn0  14867  revco  14871  cshco  14873  ofccat  15006  relexpsucl  15068  dfrtrclrec2  15095  cjreb  15174  recj  15175  imcj  15183  imval2  15202  sqrtmul  15310  absmax  15381  amgm2  15421  summolem2a  15766  fsumf1o  15774  sumsnf  15794  sumsplit  15819  fsummulc2  15835  binom  15884  bcxmas  15889  incexclem  15890  incexc  15891  expcnv  15918  pwdif  15922  cvgrat  15937  prodmolem3  15987  prodmolem2a  15988  fprodf1o  16000  prodsn  16016  prodsnf  16018  fprodabs  16028  binomfallfac  16095  fallfacval4  16097  bcfallfac  16098  ege2le3  16144  efaddlem  16147  eftlub  16165  tanval3  16190  tanneg  16204  cosmul  16229  cos01bnd  16242  demoivreALT  16257  flodddiv4  16473  absmulgcd  16607  nn0expgcd  16622  lcmfunsnlem2  16698  eulerthlem2  16841  phisum  16850  pythagtriplem14  16888  pythagtriplem19  16893  pcmul  16911  pcfac  16959  prmreclem6  16981  4sqlem12  17016  vdwlem6  17046  oppccatid  17775  curf2ndf  18303  oppcyon  18325  joincomALT  18455  meetcomALT  18457  pwsco1mhm  18891  sgrp2nmndlem4  18990  qusgrp2  19124  mulgnngsum  19145  mulgnn0p1  19151  mulgneg  19158  mulgnn0dir  19170  qusghm  19325  gaid  19369  symgval  19441  pmtrdifellem3  19548  psgnunilem2  19565  odmulg  19626  sylow1lem2  19669  sylow2a  19689  sylow3lem1  19697  efgredleme  19813  efgcpbllemb  19825  gsumzaddlem  19991  gsumconst  20004  gsumzmhm  20007  ablsimpgfindlem1  20179  srgpcomp  20300  srgbinom  20313  rdivmuldivd  20495  c0mgm  20541  c0mhm  20542  zrrnghm  20621  imadrhmcl  20878  lmodvsmmulgdi  20996  lmodsubdi  21018  rmodislmodlem  21028  0lmhm  21139  lspsneq  21224  qusrhm  21386  quscrng  21394  zringlpirlem3  21583  mulgrhm  21596  phssip  21777  frlmip  21897  frlmphl  21900  asclmulg  22021  resspsrmul  22094  evlsscasrng  22225  psdadd  22295  psdvsca  22296  psdmul  22298  psdpw  22302  psropprmul  22366  evls1scasrng  22468  mat1ghm  22609  mat1mhm  22610  1marepvmarrepid  22701  mdetrlin  22728  mdetrsca2  22730  mdetunilem7  22744  mdetunilem9  22746  mndifsplit  22762  maducoeval2  22766  smadiadetglem2  22798  decpmatmul  22898  pm2mpghm  22942  pm2mpmhmlem2  22945  cpmidgsum2  23005  ptbasfi  23707  ptuni  23720  alexsubALTlem3  24175  subgtgp  24231  tsmsxplem1  24279  xmsusp  24695  restmetu  24696  nminv  24747  nrginvrcnlem  24817  copco  25146  pcoass  25152  pi1bas  25166  pi1xfrf  25181  pi1xfr  25183  isclmp  25225  cph2subdi  25338  cphassr  25340  tcphcphlem1  25363  cphipval  25371  rrxip  25518  rrxnm  25519  pjthlem1  25565  ovolunlem1a  25624  ovolfs2  25699  uniiccdif  25706  ismbf  25756  itgaddlem2  25952  ditgswap  25987  ply1divex  26263  plyeq0lem  26336  plymullem1  26340  dgrcolem1  26399  dgrcolem2  26400  vieta1lem2  26441  elqaalem2  26450  elqaalem3  26451  aaliou3lem7  26479  ulmshft  26519  mulcxplem  26815  cxpmul2  26820  root1eq1  26886  cxpeq  26888  logbchbase  26902  cosangneg2d  26938  isosctrlem2  26950  angpieqvdlem  26959  chordthmlem3  26965  chordthmlem4  26966  chordthmlem5  26967  quad2  26970  dcubic2  26975  cubic2  26979  quart1  26987  scvxcvx  27116  igamlgam  27180  lgam1  27194  basellem9  27219  ppifl  27290  mumul  27311  sgmmul  27331  chtublem  27341  chpub  27350  logfacrlim  27354  dchrsum2  27398  sumdchr2  27400  bposlem9  27422  lgsdir2  27460  lgsdir  27462  lgsdi  27464  lgsdirnn0  27474  lgsdinn0  27475  lgsquad3  27517  2sqblem  27561  chpo1ub  27610  dchrmusum2  27624  dchrvmasumlem1  27625  dchrvmasum2if  27627  dchrisum0fmul  27636  rpvmasum2  27642  mulog2sumlem1  27664  vmalogdivsum2  27668  log2sumbnd  27674  selberg3lem1  27687  selberg4lem1  27690  pntrsumo1  27695  selbergr  27698  pntpbnd1  27716  pntlemk  27736  lesubsd  28255  mulsunif2lem  28328  divsasswd  28362  absmuls  28403  eucliddivs  28535  zcuts  28566  expsp1  28588  expadds  28594  pw2divsrecd  28606  pw2cut2  28621  bdayfinbndlem1  28626  tgbtwnconn1lem3  28809  mideulem2  28974  axlowdimlem16  29248  axcontlem8  29262  vtxval  29291  iedgval  29292  edgval  29340  vtxdgop  29761  finsumvtxdg2size  29841  lp1cycl  30444  ex-ind-dvds  30753  vsfval  30926  lnocoi  31050  nmblolbii  31092  ipasslem5  31128  hvsubid  31319  sshjval3  31647  pjhthlem1  31684  adjval  32183  unopf1o  32209  kbpj  32249  lnopmi  32293  nmcoplbi  32321  cnlnadjlem2  32361  adjadd  32386  branmfn  32398  pjtoi  32472  fconst7v  32906  ofoprabco  32950  supppreima  32977  sgnval2  33021  hashxpe  33093  ccatws1f1o  33212  splfv3  33219  xrsmulgzz  33270  mndractfo  33290  mndlactf1o  33291  mndractf1o  33292  gsumfs2d  33322  psgnfzto1stlem  33361  cycpmco2lem5  33391  cycpmco2lem6  33392  cyc3co2  33401  tocyccntz  33405  cyc3genpmlem  33412  cyc3conja  33418  archiabllem1a  33452  gsumvsca1  33487  gsumvsca2  33488  elrgspnlem2  33504  elrgspnsubrunlem1  33508  rloccring  33532  imaslmod  33616  elrspunidl  33680  mxidlirredi  33699  opprabs  33709  qsdrngi  33722  1arithidomlem1  33770  1arithidomlem2  33771  zringfrac  33789  ressply1evls1  33800  deg1prod  33818  psrbasfsupp  33846  selvply1rhmlem4  33858  mplvrpmga  33880  esplyind  33910  vietalem  33914  vieta  33915  ply1degltdimlem  33957  fedgmullem1  33964  fldextrspunlsplem  34008  extdgfialglem2  34028  algextdeglem4  34055  constrconj  34080  constrdircl  34100  constrremulcl  34102  constrimcl  34105  constrresqrtcl  34112  cos9thpiminplylem2  34118  submat1n  34140  submatres  34141  madjusmdetlem3  34164  xrge0iifhom  34272  qqhval2lem  34316  qqhrhm  34324  qqhucn  34327  esumsnf  34399  measvunilem0  34548  carsgclctunlem1  34652  ballotlemfp1  34827  ballotlemsf1o  34849  signstfveq0  34909  breprexplemc  34964  breprexp  34965  breprexpnat  34966  circlemeth  34972  logdivsqrle  34982  hgt750lema  34989  revwlk  35550  cvmlift3lem2  35745  cvmlift3lem4  35747  cvmlift3lem5  35748  cvmlift3lem6  35749  cvmlift3lem9  35752  elmrsubrn  35945  bccolsum  36164  bj-bary1lem  37876  qdiff  37893  finixpnum  38178  poimirlem4  38197  poimirlem16  38209  poimirlem19  38212  poimirlem25  38218  mblfinlem3  38232  dvtan  38243  itg2addnc  38247  itgaddnclem2  38252  ftc1anclem6  38271  areacirclem5  38285  areacirc  38286  upixp  38302  prdsbnd2  38368  ismrer1  38411  rngoneglmul  38516  rngoisocnv  38554  ecun  38966  islshpsm  39678  lshpnel2N  39683  lfl0f  39767  ldualvsdi1  39841  ldualgrplem  39843  cmtcomlemN  39946  cvlsupr8  40047  pmodl42N  40549  pmapjat1  40551  llnmod2i2  40561  dalawlem2  40570  pmapj2N  40627  idltrn  40848  cdlemc6  40894  cdleme20d  41010  cdleme22e  41042  cdleme22eALTN  41043  cdleme35b  41148  cdleme48fvg  41198  cdlemg4d  41311  cdlemg8a  41325  cdlemg42  41427  cdlemg47a  41432  tendodi1  41482  tendodi2  41483  cdlemk4  41532  cdlemk21N  41571  cdlemk22  41591  cdlemky  41624  cdlemk53b  41654  cdlemk53  41655  cdlemkyyN  41660  erngdvlem3-rN  41696  tendocnv  41719  dia1dim2  41760  dicvaddcl  41888  dihglblem3N  41993  dihmeetlem4preN  42004  dihmeet2  42044  lcfl7lem  42197  baerlem3lem1  42405  baerlem5alem1  42406  mapdh6bN  42435  mapdh6cN  42436  mapdh6dN  42437  hdmap1l6b  42509  hdmap1l6c  42510  hdmap1l6d  42511  hdmap14lem13  42578  ofun  42930  rediv23d  43146  grpcominv1  43206  evlselv  43247  flt4lem7  43317  3cubeslem2  43342  3cubeslem3r  43344  3cubeslem4  43346  pellexlem2  43483  rmxyneg  43573  oddcomabszz  43597  acongeq  43636  hausgraph  43858  onsupnmax  43881  tfsconcatrev  44001  naddass1  44046  fsovrfovd  44661  inductionexd  44807  expgrowth  44971  binomcxplemwb  44984  binomcxplemnn0  44985  binomcxplemnotnn0  44992  sumsnd  45672  restuni4  45765  fmuldfeqlem1  46224  cncfmptss  46229  climexp  46247  dvresntr  46558  stoweidlem17  46657  wallispi  46710  dirkertrigeq  46741  dirkercncflem2  46744  fourierdlem30  46777  fourierdlem41  46788  fourierdlem81  46827  fourierdlem103  46849  sge0xp  47069  sge0isummpt2  47072  isomennd  47171  vonioolem1  47320  sigarperm  47500  sin3t  47531  sin5tlem5  47537  fcores  47727  imasetpreimafvbijlemfo  48077  fundcmpsurbijinjpreimafv  48079  fundcmpsurinjimaid  48083  prprspr2  48190  ppivalnn  48307  opoeALTV  48371  uhgrimisgrgric  48619  isubgr3stgrlem2  48655  cznrng  48949  rngchomrnghmresALTV  48967  fdmdifeqresdif  49041  lincsum  49128  lincscm  49129  lmod1lem4  49189  blennngt2o2  49291  blennn0e2  49293  tposideq  49585  topdlat  49701  sectpropdlem  49733  invpropdlem  49735  isopropdlem  49737  imaidfu  49807  imasubc  49848  natoppf  49926  swapfid  49976  swapfcoa  49978  fucoppcid  50105  fucoppcco  50106  oppfdiag1  50111  diag1f1olem  50230  oppgoppchom  50287  oppgoppcco  50288  oppgoppcid  50289  2arwcat  50297  reccot  50455  rectan  50456  cotsqcscsq  50459  amgmlemALT  50511