Theorem 3eqtr4rd 2806

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752

This theorem is used by:  csbun  4399  csbdif  4481  csbcnvgALTOLD  5868  csbres  5975  fimacnvinrn2  7066  f1ossf1o  7123  suppvalbr  8163  odi  8569  phplem2  9202  cantnfp1lem3  9662  cantnfp1  9663  cardidm  9967  ackbij2lem2  10244  ackbij2lem3  10245  divneg  11933  xadddilem  13349  xadddi2  13352  dfceil2  13903  modlt  13944  modmulnn  13953  seqcaopr3  14104  bcval5  14385  hashgadd  14444  hashun3  14451  hashmap  14503  seqcoll  14532  revccat  14838  cshwmodn  14869  2cshwcom  14890  cshimadifsn0  14904  revco  14908  cshco  14910  ofccat  15045  relexpsucl  15107  dfrtrclrec2  15134  cjreb  15213  recj  15214  imcj  15222  imval2  15241  sqrtmul  15349  absmax  15420  amgm2  15460  summolem2a  15804  fsumf1o  15812  sumsnf  15832  sumsplit  15857  fsummulc2  15873  binom  15922  bcxmas  15927  incexclem  15928  incexc  15929  expcnv  15956  pwdif  15960  cvgrat  15975  prodmolem3  16023  prodmolem2a  16024  fprodf1o  16036  prodsn  16052  prodsnf  16054  fprodabs  16064  binomfallfac  16130  fallfacval4  16132  bcfallfac  16133  ege2le3  16179  efaddlem  16182  eftlub  16200  tanval3  16225  tanneg  16239  cosmul  16264  cos01bnd  16277  demoivreALT  16292  flodddiv4  16508  absmulgcd  16642  nn0expgcd  16657  lcmfunsnlem2  16733  eulerthlem2  16876  phisum  16885  pythagtriplem14  16923  pythagtriplem19  16928  pcmul  16946  pcfac  16994  prmreclem6  17016  4sqlem12  17051  vdwlem6  17081  oppccatid  17810  curf2ndf  18338  oppcyon  18360  joincomALT  18490  meetcomALT  18492  pwsco1mhm  18944  sgrp2nmndlem4  19043  qusgrp2  19184  mulgnngsum  19205  mulgnn0p1  19211  mulgneg  19218  mulgnn0dir  19230  qusghm  19385  gaid  19429  symgval  19501  pmtrdifellem3  19608  psgnunilem2  19625  odmulg  19686  sylow1lem2  19729  sylow2a  19749  sylow3lem1  19757  efgredleme  19873  efgcpbllemb  19885  gsumzaddlem  20051  gsumconst  20064  gsumzmhm  20067  ablsimpgfindlem1  20239  srgpcomp  20360  srgbinom  20373  rdivmuldivd  20557  c0mgm  20603  c0mhm  20604  zrrnghm  20701  imadrhmcl  20966  lmodvsmmulgdi  21084  lmodsubdi  21106  rmodislmodlem  21116  0lmhm  21227  lspsneq  21312  qusrhm  21481  quscrng  21489  zringlpirlem3  21680  mulgrhm  21693  phssip  21874  frlmip  21994  frlmphl  21997  asclmulg  22120  resspsrmul  22193  evlsscasrng  22324  psdadd  22394  psdvsca  22395  psdmul  22397  psdpw  22401  psropprmul  22465  evls1scasrng  22567  mat1ghm  22708  mat1mhm  22709  1marepvmarrepid  22800  mdetrlin  22827  mdetrsca2  22829  mdetunilem7  22843  mdetunilem9  22845  mndifsplit  22861  maducoeval2  22865  smadiadetglem2  22897  decpmatmul  23000  pm2mpghm  23044  pm2mpmhmlem2  23047  cpmidgsum2  23107  ptbasfi  23810  ptuni  23823  alexsubALTlem3  24278  subgtgp  24334  tsmsxplem1  24382  xmsusp  24798  restmetu  24799  nminv  24850  nrginvrcnlem  24920  copco  25249  pcoass  25255  pi1bas  25269  pi1xfrf  25284  pi1xfr  25286  isclmp  25328  cph2subdi  25441  cphassr  25443  tcphcphlem1  25466  cphipval  25474  rrxip  25621  rrxnm  25622  pjthlem1  25668  ovolunlem1a  25727  ovolfs2  25802  uniiccdif  25809  ismbf  25859  itgaddlem2  26054  ditgswap  26089  ply1divex  26365  plyeq0lem  26439  plymullem1  26443  dgrcolem1  26502  dgrcolem2  26503  vieta1lem2  26546  elqaalem2  26555  elqaalem3  26556  aaliou3lem7  26588  ulmshft  26629  mulcxplem  26924  cxpmul2  26929  root1eq1  26995  cxpeq  26997  logbchbase  27011  cosangneg2d  27047  isosctrlem2  27059  angpieqvdlem  27068  chordthmlem3  27074  chordthmlem4  27075  chordthmlem5  27076  quad2  27079  dcubic2  27084  cubic2  27088  quart1  27096  scvxcvx  27225  igamlgam  27289  lgam1  27303  basellem9  27328  ppifl  27399  mumul  27420  sgmmul  27440  chtublem  27450  chpub  27459  logfacrlim  27463  dchrsum2  27507  sumdchr2  27509  bposlem9  27531  lgsdir2  27569  lgsdir  27571  lgsdi  27573  lgsdirnn0  27583  lgsdinn0  27584  lgsquad3  27626  2sqblem  27670  chpo1ub  27719  dchrmusum2  27733  dchrvmasumlem1  27734  dchrvmasum2if  27736  dchrisum0fmul  27745  rpvmasum2  27751  mulog2sumlem1  27773  vmalogdivsum2  27777  log2sumbnd  27783  selberg3lem1  27796  selberg4lem1  27799  pntrsumo1  27804  selbergr  27807  pntpbnd1  27825  pntlemk  27845  lesubsd  28364  mulsunif2lem  28437  divsasswd  28471  absmuls  28512  eucliddivs  28644  zcuts  28675  expsp1  28697  expadds  28703  pw2divsrecd  28715  pw2cut2  28730  bdayfinbndlem1  28735  tgbtwnconn1lem3  28919  mideulem2  29092  axlowdimlem16  29417  axcontlem8  29431  vtxval  29460  iedgval  29461  edgval  29509  vtxdgop  29933  finsumvtxdg2size  30013  revwlk  30149  lp1cycl  30625  ex-ind-dvds  30944  vsfval  31117  lnocoi  31241  nmblolbii  31283  ipasslem5  31319  hvsubid  31510  sshjval3  31838  pjhthlem1  31875  adjval  32374  unopf1o  32400  kbpj  32440  lnopmi  32484  nmcoplbi  32512  cnlnadjlem2  32552  adjadd  32577  branmfn  32589  pjtoi  32663  fconst7v  33096  ofoprabco  33140  supppreima  33166  sgnval2  33209  hashxpe  33281  ccatws1f1o  33396  splfv3  33401  xrsmulgzz  33452  mndractfo  33472  mndlactf1o  33473  mndractf1o  33474  gsumfs2d  33504  psgnfzto1stlem  33543  cycpmco2lem5  33573  cycpmco2lem6  33574  cyc3co2  33583  tocyccntz  33587  cyc3genpmlem  33594  cyc3conja  33600  archiabllem1a  33634  gsumvsca1  33669  gsumvsca2  33670  elrgspnlem2  33686  elrgspnsubrunlem1  33690  rloccring  33714  imaslmod  33796  elrspunidl  33859  mxidlirredi  33877  opprabs  33887  qsdrngi  33900  1arithidomlem1  33948  1arithidomlem2  33949  zringfrac  33967  ressply1evls1  33978  deg1prod  33996  psrbasfsupp  34024  selvply1rhmlem4  34036  mplvrpmga  34058  esplyind  34088  vietalem  34092  vieta  34093  ply1degltdimlem  34135  fedgmullem1  34142  fldextrspunlsplem  34186  extdgfialglem2  34206  algextdeglem4  34233  constrconj  34258  constrdircl  34278  constrremulcl  34280  constrimcl  34283  constrresqrtcl  34290  cos9thpiminplylem2  34296  submat1n  34318  submatres  34319  madjusmdetlem3  34342  xrge0iifhom  34450  qqhval2lem  34494  qqhrhm  34502  qqhucn  34505  esumsnf  34577  measvunilem0  34727  carsgclctunlem1  34831  ballotlemfp1  35006  ballotlemsf1o  35028  signstfveq0  35088  breprexplemc  35143  breprexp  35144  breprexpnat  35145  circlemeth  35151  logdivsqrle  35161  hgt750lema  35168  cvmlift3lem2  35902  cvmlift3lem4  35904  cvmlift3lem5  35905  cvmlift3lem6  35906  cvmlift3lem9  35909  elmrsubrn  36102  bccolsum  36321  bj-bary1lem  38065  qdiff  38082  finixpnum  38362  poimirlem4  38376  poimirlem16  38388  poimirlem19  38391  poimirlem25  38397  mblfinlem3  38411  dvtan  38422  itg2addnc  38426  itgaddnclem2  38431  ftc1anclem6  38450  areacirclem5  38464  areacirc  38465  upixp  38482  prdsbnd2  38548  ismrer1  38591  rngoneglmul  38696  rngoisocnv  38734  ecun  39144  islshpsm  39856  lshpnel2N  39861  lfl0f  39945  ldualvsdi1  40019  ldualgrplem  40021  cmtcomlemN  40124  cvlsupr8  40225  pmodl42N  40727  pmapjat1  40729  llnmod2i2  40739  dalawlem2  40748  pmapj2N  40805  idltrn  41026  cdlemc6  41072  cdleme20d  41188  cdleme22e  41220  cdleme22eALTN  41221  cdleme35b  41326  cdleme48fvg  41376  cdlemg4d  41489  cdlemg8a  41503  cdlemg42  41605  cdlemg47a  41610  tendodi1  41660  tendodi2  41661  cdlemk4  41710  cdlemk21N  41749  cdlemk22  41769  cdlemky  41802  cdlemk53b  41832  cdlemk53  41833  cdlemkyyN  41838  erngdvlem3-rN  41874  tendocnv  41897  dia1dim2  41938  dicvaddcl  42066  dihglblem3N  42171  dihmeetlem4preN  42182  dihmeet2  42222  lcfl7lem  42375  baerlem3lem1  42583  baerlem5alem1  42584  mapdh6bN  42613  mapdh6cN  42614  mapdh6dN  42615  hdmap1l6b  42687  hdmap1l6c  42688  hdmap1l6d  42689  hdmap14lem13  42756  ofun  43108  rediv23d  43339  grpcominv1  43399  evlselv  43438  flt4lem7  43508  3cubeslem2  43533  3cubeslem3r  43535  3cubeslem4  43537  pellexlem2  43674  rmxyneg  43764  oddcomabszz  43788  acongeq  43827  hausgraph  44049  onsupnmax  44072  tfsconcatrev  44192  naddass1  44237  fsovrfovd  44852  inductionexd  44998  expgrowth  45162  binomcxplemwb  45175  binomcxplemnn0  45176  binomcxplemnotnn0  45183  sumsnd  45863  restuni4  45956  fmuldfeqlem1  46415  cncfmptss  46420  climexp  46438  dvresntr  46749  stoweidlem17  46848  wallispi  46901  dirkertrigeq  46932  dirkercncflem2  46935  fourierdlem30  46968  fourierdlem41  46979  fourierdlem81  47018  fourierdlem103  47040  sge0xp  47260  sge0isummpt2  47263  isomennd  47362  vonioolem1  47511  sigarperm  47691  sin3t  47738  sin5tlem5  47744  fcores  47958  imasetpreimafvbijlemfo  48308  fundcmpsurbijinjpreimafv  48310  fundcmpsurinjimaid  48314  prprspr2  48421  ppivalnn  48538  opoeALTV  48602  uhgrimisgrgric  48850  isubgr3stgrlem2  48886  cznrng  49179  rngchomrnghmresALTV  49197  fdmdifeqresdif  49275  lincsum  49362  lincscm  49363  lmod1lem4  49423  blennngt2o2  49525  blennn0e2  49527  tposideq  49817  topdlat  49933  sectpropdlem  49965  invpropdlem  49967  isopropdlem  49969  imaidfu  50039  imasubc  50080  natoppf  50158  swapfid  50208  swapfcoa  50210  fucoppcid  50337  fucoppcco  50338  oppfdiag1  50343  diag1f1olem  50462  oppgoppchom  50519  oppgoppcco  50520  oppgoppcid  50521  2arwcat  50529  reccot  50687  rectan  50688  cotsqcscsq  50691  crosspaltd  50802  crossp3d  50803  amgmlemALT  50824