Theorem 3eqtr4rd 2807

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

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

This theorem is used by:  csbun  4399  csbdif  4481  csbcnvgALTOLD  5866  csbres  5973  fimacnvinrn2  7072  f1ossf1o  7129  suppvalbr  8181  odi  8587  phplem2  9220  cantnfp1lem3  9681  cantnfp1  9682  cardidm  10040  ackbij2lem2  10317  ackbij2lem3  10318  divneg  12008  xadddilem  13424  xadddi2  13427  dfceil2  13979  modlt  14020  modmulnn  14029  seqcaopr3  14180  bcval5  14462  hashgadd  14521  hashun3  14528  hashmap  14580  seqcoll  14609  revccat  14915  cshwmodn  14946  2cshwcom  14967  cshimadifsn0  14981  revco  14985  cshco  14987  ofccat  15122  relexpsucl  15184  dfrtrclrec2  15211  cjreb  15290  recj  15291  imcj  15299  imval2  15318  sqrtmul  15426  absmax  15497  amgm2  15537  summolem2a  15881  fsumf1o  15889  sumsnf  15909  sumsplit  15934  fsummulc2  15950  binom  15999  bcxmas  16004  incexclem  16005  incexc  16006  expcnv  16033  pwdif  16037  cvgrat  16052  prodmolem3  16100  prodmolem2a  16101  fprodf1o  16113  prodsn  16129  prodsnf  16131  fprodabs  16141  binomfallfac  16207  fallfacval4  16209  bcfallfac  16210  ege2le3  16256  efaddlem  16259  eftlub  16277  tanval3  16302  tanneg  16316  cosmul  16341  cos01bnd  16354  demoivreALT  16369  flodddiv4  16585  absmulgcd  16722  nn0expgcd  16738  lcmfunsnlem2  16815  eulerthlem2  16959  phisum  16968  pythagtriplem14  17006  pythagtriplem19  17011  pcmul  17029  pcfac  17077  prmreclem6  17099  4sqlem12  17134  vdwlem6  17164  oppccatid  17893  curf2ndf  18421  oppcyon  18443  joincomALT  18573  meetcomALT  18575  pwsco1mhm  19028  sgrp2nmndlem4  19127  qusgrp2  19268  mulgnngsum  19289  mulgnn0p1  19295  mulgneg  19302  mulgnn0dir  19314  qusghm  19469  gaid  19513  symgval  19585  pmtrdifellem3  19692  psgnunilem2  19709  odmulg  19770  sylow1lem2  19813  sylow2a  19833  sylow3lem1  19841  efgredleme  19957  efgcpbllemb  19969  gsumzaddlem  20135  gsumconst  20148  gsumzmhm  20151  ablsimpgfindlem1  20323  srgpcomp  20444  srgbinom  20457  rdivmuldivd  20643  c0mgm  20689  c0mhm  20690  zrrnghm  20788  imadrhmcl  21054  lmodvsmmulgdi  21172  lmodsubdi  21194  rmodislmodlem  21204  0lmhm  21315  lspsneq  21400  qusrhm  21570  quscrng  21579  zringlpirlem3  21770  mulgrhm  21783  phssip  21964  frlmip  22084  frlmphl  22087  asclmulg  22210  resspsrmul  22283  evlsscasrng  22414  psdadd  22484  psdvsca  22485  psdmul  22487  psdpw  22491  psropprmul  22555  evls1scasrng  22657  mat1ghm  22798  mat1mhm  22799  1marepvmarrepid  22890  mdetrlin  22917  mdetrsca2  22919  mdetunilem7  22933  mdetunilem9  22935  mndifsplit  22951  maducoeval2  22955  smadiadetglem2  22987  decpmatmul  23090  pm2mpghm  23134  pm2mpmhmlem2  23137  cpmidgsum2  23197  ptbasfi  23900  ptuni  23913  alexsubALTlem3  24368  subgtgp  24424  tsmsxplem1  24472  xmsusp  24888  restmetu  24889  nminv  24940  nrginvrcnlem  25010  copco  25339  pcoass  25345  pi1bas  25359  pi1xfrf  25374  pi1xfr  25376  isclmp  25418  cph2subdi  25531  cphassr  25533  tcphcphlem1  25556  cphipval  25564  rrxip  25711  rrxnm  25712  pjthlem1  25758  ovolunlem1a  25817  ovolfs2  25892  uniiccdif  25899  ismbf  25949  itgaddlem2  26144  ditgswap  26179  ply1divex  26455  plyeq0lem  26529  plymullem1  26533  dgrcolem1  26592  dgrcolem2  26593  vieta1lem2  26634  elqaalem2  26643  elqaalem3  26644  aaliou3lem7  26676  ulmshft  26717  mulcxplem  27012  cxpmul2  27017  root1eq1  27083  cxpeq  27085  logbchbase  27099  cosangneg2d  27135  isosctrlem2  27147  angpieqvdlem  27156  chordthmlem3  27162  chordthmlem4  27163  chordthmlem5  27164  quad2  27167  dcubic2  27172  cubic2  27176  quart1  27184  scvxcvx  27313  igamlgam  27377  lgam1  27391  basellem9  27416  ppifl  27487  mumul  27508  sgmmul  27528  chtublem  27538  chpub  27547  logfacrlim  27551  dchrsum2  27595  sumdchr2  27597  bposlem9  27619  lgsdir2  27657  lgsdir  27659  lgsdi  27661  lgsdirnn0  27671  lgsdinn0  27672  lgsquad3  27714  2sqblem  27758  chpo1ub  27807  dchrmusum2  27821  dchrvmasumlem1  27822  dchrvmasum2if  27824  dchrisum0fmul  27833  rpvmasum2  27839  mulog2sumlem1  27861  vmalogdivsum2  27865  log2sumbnd  27871  selberg3lem1  27884  selberg4lem1  27887  pntrsumo1  27892  selbergr  27895  pntpbnd1  27913  pntlemk  27933  flt4lem7  27989  lesubsd  28482  mulsunif2lem  28555  divsasswd  28589  absmuls  28630  eucliddivs  28762  zcuts  28793  expsp1  28815  expadds  28821  pw2divsrecd  28833  pw2cut2  28848  bdayfinbndlem1  28853  tgbtwnconn1lem3  29037  mideulem2  29210  axlowdimlem16  29535  axcontlem8  29549  vtxval  29578  iedgval  29579  edgval  29627  vtxdgop  30051  finsumvtxdg2size  30131  revwlk  30267  lp1cycl  30743  ex-ind-dvds  31062  vsfval  31235  lnocoi  31359  nmblolbii  31401  ipasslem5  31437  hvsubid  31628  sshjval3  31956  pjhthlem1  31993  adjval  32492  unopf1o  32518  kbpj  32558  lnopmi  32602  nmcoplbi  32630  cnlnadjlem2  32670  adjadd  32695  branmfn  32707  pjtoi  32781  fconst7v  33214  ofoprabco  33258  supppreima  33284  sgnval2  33327  hashxpe  33399  ccatws1f1o  33514  splfv3  33519  xrsmulgzz  33570  mndractfo  33590  mndlactf1o  33591  mndractf1o  33592  gsumfs2d  33622  psgnfzto1stlem  33661  cycpmco2lem5  33691  cycpmco2lem6  33692  cyc3co2  33701  tocyccntz  33705  cyc3genpmlem  33712  cyc3conja  33718  archiabllem1a  33752  gsumvsca1  33787  gsumvsca2  33788  elrgspnlem2  33804  elrgspnsubrunlem1  33808  rloccring  33832  imaslmod  33914  elrspunidl  33978  mxidlirredi  33996  opprabs  34006  qsdrngi  34019  1arithidomlem1  34067  1arithidomlem2  34068  zringfrac  34086  ressply1evls1  34097  deg1prod  34115  psrbasfsupp  34143  selvply1rhmlem4  34155  mplvrpmga  34177  esplyind  34207  vietalem  34211  vieta  34212  ply1degltdimlem  34254  fedgmullem1  34261  fldextrspunlsplem  34305  extdgfialglem2  34325  algextdeglem4  34352  constrconj  34377  constrdircl  34397  constrremulcl  34399  constrimcl  34402  constrresqrtcl  34409  cos9thpiminplylem2  34415  submat1n  34437  submatres  34438  madjusmdetlem3  34461  xrge0iifhom  34569  qqhval2lem  34613  qqhrhm  34621  qqhucn  34624  esumsnf  34696  measvunilem0  34846  carsgclctunlem1  34949  ballotlemfp1  35124  ballotlemsf1o  35146  signstfveq0  35206  breprexplemc  35261  breprexp  35262  breprexpnat  35263  circlemeth  35269  logdivsqrle  35279  hgt750lema  35286  cvmlift3lem2  36085  cvmlift3lem4  36087  cvmlift3lem5  36088  cvmlift3lem6  36089  cvmlift3lem9  36092  elmrsubrn  36285  bccolsum  36504  bj-bary1lem  38231  qdiff  38248  finixpnum  38528  poimirlem4  38542  poimirlem16  38554  poimirlem19  38557  poimirlem25  38563  mblfinlem3  38577  dvtan  38588  itg2addnc  38592  itgaddnclem2  38597  ftc1anclem6  38616  areacirclem5  38630  areacirc  38631  upixp  38663  prdsbnd2  38729  ismrer1  38772  rngoneglmul  38877  rngoisocnv  38915  ecun  39325  islshpsm  40037  lshpnel2N  40042  lfl0f  40126  ldualvsdi1  40200  ldualgrplem  40202  cmtcomlemN  40305  cvlsupr8  40406  pmodl42N  40908  pmapjat1  40910  llnmod2i2  40920  dalawlem2  40929  pmapj2N  40986  idltrn  41207  cdlemc6  41253  cdleme20d  41369  cdleme22e  41401  cdleme22eALTN  41402  cdleme35b  41507  cdleme48fvg  41557  cdlemg4d  41670  cdlemg8a  41684  cdlemg42  41786  cdlemg47a  41791  tendodi1  41841  tendodi2  41842  cdlemk4  41891  cdlemk21N  41930  cdlemk22  41950  cdlemky  41983  cdlemk53b  42013  cdlemk53  42014  cdlemkyyN  42019  erngdvlem3-rN  42055  tendocnv  42078  dia1dim2  42119  dicvaddcl  42247  dihglblem3N  42352  dihmeetlem4preN  42363  dihmeet2  42403  lcfl7lem  42556  baerlem3lem1  42764  baerlem5alem1  42765  mapdh6bN  42794  mapdh6cN  42795  mapdh6dN  42796  hdmap1l6b  42868  hdmap1l6c  42869  hdmap1l6d  42870  hdmap14lem13  42937  ofun  43289  rediv23d  43512  grpcominv1  43575  evlselv  43617  3cubeslem2  43695  3cubeslem3r  43697  3cubeslem4  43699  pellexlem2  43836  rmxyneg  43926  oddcomabszz  43950  acongeq  43989  hausgraph  44206  onsupnmax  44229  tfsconcatrev  44349  naddass1  44394  fsovrfovd  45008  inductionexd  45154  expgrowth  45318  binomcxplemwb  45331  binomcxplemnn0  45332  binomcxplemnotnn0  45339  sumsnd  46042  restuni4  46135  fmuldfeqlem1  46593  cncfmptss  46598  climexp  46616  dvresntr  46927  stoweidlem17  47026  wallispi  47079  dirkertrigeq  47110  dirkercncflem2  47113  fourierdlem30  47146  fourierdlem41  47157  fourierdlem81  47196  fourierdlem103  47218  sge0xp  47438  sge0isummpt2  47441  isomennd  47540  vonioolem1  47689  sigarperm  47869  sin3t  47916  sin5tlem5  47922  fcores  48136  imasetpreimafvbijlemfo  48486  fundcmpsurbijinjpreimafv  48488  fundcmpsurinjimaid  48492  prprspr2  48599  ppivalnn  48716  opoeALTV  48780  uhgrimisgrgric  49028  isubgr3stgrlem2  49064  cznrng  49357  rngchomrnghmresALTV  49375  fdmdifeqresdif  49453  lincsum  49540  lincscm  49541  lmod1lem4  49601  blennngt2o2  49703  blennn0e2  49705  tposideq  49995  topdlat  50111  sectpropdlem  50143  invpropdlem  50145  isopropdlem  50147  imaidfu  50217  imasubc  50258  natoppf  50336  swapfid  50386  swapfcoa  50388  fucoppcid  50515  fucoppcco  50516  oppfdiag1  50521  diag1f1olem  50640  oppgoppchom  50697  oppgoppcco  50698  oppgoppcid  50699  2arwcat  50707  reccot  50850  rectan  50851  cotsqcscsq  50854  crosspaltd  50965  crossp3d  50966  amgmlemALT  50987