Theorem 3eqtr4rd 2809

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755

This theorem is used by:  csbun  4401  csbdif  4483  csbcnvgALTOLD  5870  csbres  5977  fimacnvinrn2  7080  f1ossf1o  7137  suppvalbrOLD  8192  odi  8598  phplem2  9231  cantnfp1lem3  9691  cantnfp1  9692  cardidm  10050  ackbij2lem2  10327  ackbij2lem3  10328  divneg  12018  xadddilem  13434  xadddi2  13437  dfceil2  13989  modlt  14030  modmulnn  14039  seqcaopr3  14190  bcval5  14472  hashgadd  14531  hashun3  14538  hashmap  14590  seqcoll  14619  revccat  14926  cshwmodn  14957  2cshwcom  14978  cshimadifsn0  14992  revco  14996  cshco  14998  ofccat  15134  relexpsucl  15196  dfrtrclrec2  15223  cjreb  15302  recj  15303  imcj  15311  imval2  15330  sqrtmul  15438  absmax  15509  amgm2  15549  summolem2a  15893  fsumf1o  15901  sumsnf  15921  sumsplit  15946  fsummulc2  15962  binom  16011  bcxmas  16016  incexclem  16017  incexc  16018  expcnv  16045  pwdif  16049  cvgrat  16064  prodmolem3  16112  prodmolem2a  16113  fprodf1o  16125  prodsn  16141  prodsnf  16143  fprodabs  16153  binomfallfac  16219  fallfacval4  16221  bcfallfac  16222  ege2le3  16268  efaddlem  16271  eftlub  16289  tanval3  16314  tanneg  16328  cosmul  16353  cos01bnd  16366  demoivreALT  16381  flodddiv4  16597  absmulgcd  16734  nn0expgcd  16750  lcmfunsnlem2  16827  eulerthlem2  16971  phisum  16980  pythagtriplem14  17018  pythagtriplem19  17023  pcmul  17041  pcfac  17089  prmreclem6  17111  4sqlem12  17146  vdwlem6  17176  oppccatid  17905  curf2ndf  18433  oppcyon  18455  joincomALT  18585  meetcomALT  18587  pwsco1mhm  19040  sgrp2nmndlem4  19139  qusgrp2  19280  mulgnngsum  19301  mulgnn0p1  19307  mulgneg  19314  mulgnn0dir  19326  qusghm  19481  gaid  19525  symgval  19597  pmtrdifellem3  19704  psgnunilem2  19721  odmulg  19782  sylow1lem2  19825  sylow2a  19845  sylow3lem1  19853  efgredleme  19969  efgcpbllemb  19981  gsumzaddlem  20147  gsumconst  20160  gsumzmhm  20163  ablsimpgfindlem1  20335  srgpcomp  20456  srgbinom  20469  rdivmuldivd  20655  c0mgm  20701  c0mhm  20702  zrrnghm  20800  imadrhmcl  21066  lmodvsmmulgdi  21184  lmodsubdi  21206  rmodislmodlem  21216  0lmhm  21327  lspsneq  21412  qusrhm  21582  quscrng  21591  zringlpirlem3  21782  mulgrhm  21795  phssip  21976  frlmip  22096  frlmphl  22099  asclmulg  22222  resspsrmul  22295  evlsscasrng  22426  psdadd  22496  psdvsca  22497  psdmul  22499  psdpw  22503  psropprmul  22567  evls1scasrng  22669  mat1ghm  22810  mat1mhm  22811  1marepvmarrepid  22902  mdetrlin  22929  mdetrsca2  22931  mdetunilem7  22945  mdetunilem9  22947  mndifsplit  22963  maducoeval2  22967  smadiadetglem2  22999  decpmatmul  23102  pm2mpghm  23146  pm2mpmhmlem2  23149  cpmidgsum2  23209  ptbasfi  23912  ptuni  23925  alexsubALTlem3  24380  subgtgp  24436  tsmsxplem1  24484  xmsusp  24900  restmetu  24901  nminv  24952  nrginvrcnlem  25022  copco  25351  pcoass  25357  pi1bas  25371  pi1xfrf  25386  pi1xfr  25388  isclmp  25430  cph2subdi  25543  cphassr  25545  tcphcphlem1  25568  cphipval  25576  rrxip  25723  rrxnm  25724  pjthlem1  25770  ovolunlem1a  25829  ovolfs2  25904  uniiccdif  25911  ismbf  25961  itgaddlem2  26156  ditgswap  26191  ply1divex  26467  plyeq0lem  26541  plymullem1  26545  dgrcolem1  26604  dgrcolem2  26605  vieta1lem2  26646  elqaalem2  26655  elqaalem3  26656  aaliou3lem7  26688  ulmshft  26729  mulcxplem  27024  cxpmul2  27029  root1eq1  27095  cxpeq  27097  logbchbase  27111  cosangneg2d  27147  isosctrlem2  27159  angpieqvdlem  27168  chordthmlem3  27174  chordthmlem4  27175  chordthmlem5  27176  quad2  27179  dcubic2  27184  cubic2  27188  quart1  27196  scvxcvx  27325  igamlgam  27389  lgam1  27403  basellem9  27428  ppifl  27499  mumul  27520  sgmmul  27540  chtublem  27550  chpub  27559  logfacrlim  27563  dchrsum2  27607  sumdchr2  27609  bposlem9  27631  lgsdir2  27669  lgsdir  27671  lgsdi  27673  lgsdirnn0  27683  lgsdinn0  27684  lgsquad3  27726  2sqblem  27770  chpo1ub  27819  dchrmusum2  27833  dchrvmasumlem1  27834  dchrvmasum2if  27836  dchrisum0fmul  27845  rpvmasum2  27851  mulog2sumlem1  27873  vmalogdivsum2  27877  log2sumbnd  27883  selberg3lem1  27896  selberg4lem1  27899  pntrsumo1  27904  selbergr  27907  pntpbnd1  27925  pntlemk  27945  flt4lem7  28001  lesubsd  28494  mulsunif2lem  28567  divsasswd  28601  absmuls  28642  eucliddivs  28774  zcuts  28805  expsp1  28827  expadds  28833  pw2divsrecd  28845  pw2cut2  28860  bdayfinbndlem1  28865  tgbtwnconn1lem3  29049  mideulem2  29222  axlowdimlem16  29547  axcontlem8  29561  vtxval  29590  iedgval  29591  edgval  29639  vtxdgop  30063  finsumvtxdg2size  30143  revwlk  30279  lp1cycl  30755  ex-ind-dvds  31074  vsfval  31247  lnocoi  31371  nmblolbii  31413  ipasslem5  31449  hvsubid  31640  sshjval3  31968  pjhthlem1  32005  adjval  32504  unopf1o  32530  kbpj  32570  lnopmi  32614  nmcoplbi  32642  cnlnadjlem2  32682  adjadd  32707  branmfn  32719  pjtoi  32793  fconst7v  33268  ofoprabco  33312  supppreima  33338  sgnval2  33380  hashxpe  33452  ccatws1f1o  33567  splfv3  33572  xrsmulgzz  33623  mndractfo  33643  mndlactf1o  33644  mndractf1o  33645  gsumfs2d  33675  psgnfzto1stlem  33714  cycpmco2lem5  33744  cycpmco2lem6  33745  cyc3co2  33754  tocyccntz  33758  cyc3genpmlem  33765  cyc3conja  33771  archiabllem1a  33805  gsumvsca1  33840  gsumvsca2  33841  elrgspnlem2  33857  elrgspnsubrunlem1  33861  rloccring  33885  imaslmod  33967  elrspunidl  34031  mxidlirredi  34049  opprabs  34059  qsdrngi  34072  1arithidomlem1  34120  1arithidomlem2  34121  zringfrac  34139  ressply1evls1  34150  deg1prod  34168  psrbasfsupp  34196  selvply1rhmlem4  34208  mplvrpmga  34230  esplyind  34260  vietalem  34264  vieta  34265  ply1degltdimlem  34307  fedgmullem1  34314  fldextrspunlsplem  34358  extdgfialglem2  34378  algextdeglem4  34405  constrconj  34430  constrdircl  34450  constrremulcl  34452  constrimcl  34455  constrresqrtcl  34462  cos9thpiminplylem2  34468  submat1n  34490  submatres  34491  madjusmdetlem3  34514  xrge0iifhom  34622  qqhval2lem  34666  qqhrhm  34674  qqhucn  34677  esumsnf  34749  measvunilem0  34899  carsgclctunlem1  35002  ballotlemfp1  35177  ballotlemsf1o  35199  signstfveq0  35259  breprexplemc  35314  breprexp  35315  breprexpnat  35316  circlemeth  35322  logdivsqrle  35332  hgt750lema  35339  cvmlift3lem2  36206  cvmlift3lem4  36208  cvmlift3lem5  36209  cvmlift3lem6  36210  cvmlift3lem9  36213  elmrsubrn  36406  bccolsum  36631  bj-bary1lem  38371  qdiff  38388  finixpnum  38668  poimirlem4  38682  poimirlem16  38694  poimirlem19  38697  poimirlem25  38703  mblfinlem3  38717  dvtan  38728  itg2addnc  38732  itgaddnclem2  38737  ftc1anclem6  38756  areacirclem5  38770  areacirc  38771  upixp  38803  prdsbnd2  38869  ismrer1  38912  rngoneglmul  39017  rngoisocnv  39055  ecun  39465  islshpsm  40177  lshpnel2N  40182  lfl0f  40266  ldualvsdi1  40340  ldualgrplem  40342  cmtcomlemN  40445  cvlsupr8  40546  pmodl42N  41048  pmapjat1  41050  llnmod2i2  41060  dalawlem2  41069  pmapj2N  41126  idltrn  41347  cdlemc6  41393  cdleme20d  41509  cdleme22e  41541  cdleme22eALTN  41542  cdleme35b  41647  cdleme48fvg  41697  cdlemg4d  41810  cdlemg8a  41824  cdlemg42  41926  cdlemg47a  41931  tendodi1  41981  tendodi2  41982  cdlemk4  42031  cdlemk21N  42070  cdlemk22  42090  cdlemky  42123  cdlemk53b  42153  cdlemk53  42154  cdlemkyyN  42159  erngdvlem3-rN  42195  tendocnv  42218  dia1dim2  42259  dicvaddcl  42387  dihglblem3N  42492  dihmeetlem4preN  42503  dihmeet2  42543  lcfl7lem  42696  baerlem3lem1  42904  baerlem5alem1  42905  mapdh6bN  42934  mapdh6cN  42935  mapdh6dN  42936  hdmap1l6b  43008  hdmap1l6c  43009  hdmap1l6d  43010  hdmap14lem13  43077  ofun  43429  rediv23d  43652  grpcominv1  43715  evlselv  43757  3cubeslem2  43835  3cubeslem3r  43837  3cubeslem4  43839  pellexlem2  43977  rmxyneg  44067  oddcomabszz  44091  acongeq  44130  hausgraph  44347  onsupnmax  44370  tfsconcatrev  44490  naddass1  44535  fsovrfovd  45149  inductionexd  45295  expgrowth  45459  binomcxplemwb  45472  binomcxplemnn0  45473  binomcxplemnotnn0  45480  sumsnd  46182  restuni4  46275  fmuldfeqlem1  46733  cncfmptss  46738  climexp  46756  dvresntr  47067  stoweidlem17  47166  wallispi  47219  dirkertrigeq  47250  dirkercncflem2  47253  fourierdlem30  47286  fourierdlem41  47297  fourierdlem81  47336  fourierdlem103  47358  sge0xp  47578  sge0isummpt2  47581  isomennd  47680  vonioolem1  47829  sigarperm  48009  sin3t  48056  sin5tlem5  48062  fcores  48276  imasetpreimafvbijlemfo  48626  fundcmpsurbijinjpreimafv  48628  fundcmpsurinjimaid  48632  prprspr2  48739  ppivalnn  48856  opoeALTV  48920  uhgrimisgrgric  49168  isubgr3stgrlem2  49204  cznrng  49497  rngchomrnghmresALTV  49515  fdmdifeqresdif  49593  lincsum  49680  lincscm  49681  lmod1lem4  49741  blennngt2o2  49843  blennn0e2  49845  tposideq  50140  topdlat  50257  sectpropdlem  50289  invpropdlem  50291  isopropdlem  50293  imaidfu  50365  imasubc  50406  natoppf  50490  swapfid  50540  swapfcoa  50542  fucoppcid  50682  fucoppcco  50683  oppfdiag1  50688  diag1f1olem  50807  oppgoppchom  50867  oppgoppcco  50868  oppgoppcid  50869  2arwcat  50877  parmapco2  50911  parmapco  50912  parmapfunc2  50913  reccot  51065  rectan  51066  cotsqcscsq  51069  crosspaltd  51180  crossp3d  51181  amgmlemALT  51202