Theorem 3eqtr4rd 2782

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  csbun  4381  csbdif  4465  csbcnvgALT  5839  csbres  5947  fimacnvinrn2  7024  f1ossf1o  7081  suppvalbr  8114  odi  8514  phplem2  9139  cantnfp1lem3  9601  cantnfp1  9602  cardidm  9883  ackbij2lem2  10161  ackbij2lem3  10162  divneg  11846  xadddilem  13246  xadddi2  13249  dfceil2  13798  modlt  13839  modmulnn  13848  seqcaopr3  13999  bcval5  14280  hashgadd  14339  hashun3  14346  hashmap  14397  seqcoll  14426  revccat  14728  cshwmodn  14757  2cshwcom  14778  cshimadifsn0  14792  revco  14796  cshco  14798  ofccat  14931  relexpsucl  14993  dfrtrclrec2  15020  cjreb  15085  recj  15086  imcj  15094  imval2  15113  sqrtmul  15221  absmax  15292  amgm2  15332  summolem2a  15677  fsumf1o  15685  sumsnf  15705  sumsplit  15730  fsummulc2  15746  binom  15795  bcxmas  15800  incexclem  15801  incexc  15802  expcnv  15829  pwdif  15833  cvgrat  15848  prodmolem3  15898  prodmolem2a  15899  fprodf1o  15911  prodsn  15927  prodsnf  15929  fprodabs  15939  binomfallfac  16006  fallfacval4  16008  bcfallfac  16009  ege2le3  16055  efaddlem  16058  eftlub  16076  tanval3  16101  tanneg  16115  cosmul  16140  cos01bnd  16153  demoivreALT  16168  flodddiv4  16384  absmulgcd  16518  nn0expgcd  16533  lcmfunsnlem2  16609  eulerthlem2  16752  phisum  16761  pythagtriplem14  16799  pythagtriplem19  16804  pcmul  16822  pcfac  16870  prmreclem6  16892  4sqlem12  16927  vdwlem6  16957  oppccatid  17685  curf2ndf  18213  oppcyon  18235  joincomALT  18365  meetcomALT  18367  pwsco1mhm  18800  sgrp2nmndlem4  18899  qusgrp2  19034  mulgnngsum  19055  mulgnn0p1  19061  mulgneg  19068  mulgnn0dir  19080  qusghm  19230  gaid  19274  symgval  19346  pmtrdifellem3  19453  psgnunilem2  19470  odmulg  19531  sylow1lem2  19574  sylow2a  19594  sylow3lem1  19602  efgredleme  19718  efgcpbllemb  19730  gsumzaddlem  19896  gsumconst  19909  gsumzmhm  19912  ablsimpgfindlem1  20084  srgpcomp  20199  srgbinom  20212  rdivmuldivd  20393  c0mgm  20439  c0mhm  20440  zrrnghm  20513  imadrhmcl  20774  lmodvsmmulgdi  20892  lmodsubdi  20914  rmodislmodlem  20924  0lmhm  21035  lspsneq  21120  qusrhm  21274  quscrng  21281  zringlpirlem3  21444  mulgrhm  21457  phssip  21638  frlmip  21758  frlmphl  21761  asclmulg  21882  resspsrmul  21954  evlsscasrng  22083  psdadd  22129  psdvsca  22130  psdmul  22132  psdpw  22136  psropprmul  22201  evls1scasrng  22304  mat1ghm  22448  mat1mhm  22449  1marepvmarrepid  22540  mdetrlin  22567  mdetrsca2  22569  mdetunilem7  22583  mdetunilem9  22585  mndifsplit  22601  maducoeval2  22605  smadiadetglem2  22637  decpmatmul  22737  pm2mpghm  22781  pm2mpmhmlem2  22784  cpmidgsum2  22844  ptbasfi  23546  ptuni  23559  alexsubALTlem3  24014  subgtgp  24070  tsmsxplem1  24118  xmsusp  24534  restmetu  24535  nminv  24586  nrginvrcnlem  24656  copco  24985  pcoass  24991  pi1bas  25005  pi1xfrf  25020  pi1xfr  25022  isclmp  25064  cph2subdi  25177  cphassr  25179  tcphcphlem1  25202  cphipval  25210  rrxip  25357  rrxnm  25358  pjthlem1  25404  ovolunlem1a  25463  ovolfs2  25538  uniiccdif  25545  ismbf  25595  itgaddlem2  25791  ditgswap  25826  ply1divex  26102  plyeq0lem  26175  plymullem1  26179  dgrcolem1  26238  dgrcolem2  26239  vieta1lem2  26277  elqaalem2  26286  elqaalem3  26287  aaliou3lem7  26315  ulmshft  26355  mulcxplem  26648  cxpmul2  26653  root1eq1  26719  cxpeq  26721  logbchbase  26735  cosangneg2d  26771  isosctrlem2  26783  angpieqvdlem  26792  chordthmlem3  26798  chordthmlem4  26799  chordthmlem5  26800  quad2  26803  dcubic2  26808  cubic2  26812  quart1  26820  scvxcvx  26949  igamlgam  27013  lgam1  27027  basellem9  27052  ppifl  27123  mumul  27144  sgmmul  27164  chtublem  27174  chpub  27183  logfacrlim  27187  dchrsum2  27231  sumdchr2  27233  bposlem9  27255  lgsdir2  27293  lgsdir  27295  lgsdi  27297  lgsdirnn0  27307  lgsdinn0  27308  lgsquad3  27350  2sqblem  27394  chpo1ub  27443  dchrmusum2  27457  dchrvmasumlem1  27458  dchrvmasum2if  27460  dchrisum0fmul  27469  rpvmasum2  27475  mulog2sumlem1  27497  vmalogdivsum2  27501  log2sumbnd  27507  selberg3lem1  27520  selberg4lem1  27523  pntrsumo1  27528  selbergr  27531  pntpbnd1  27549  pntlemk  27569  lesubsd  28088  mulsunif2lem  28161  divsasswd  28195  absmuls  28236  eucliddivs  28368  zcuts  28399  expsp1  28421  expadds  28427  pw2divsrecd  28439  pw2cut2  28454  bdayfinbndlem1  28459  tgbtwnconn1lem3  28642  mideulem2  28802  axlowdimlem16  29026  axcontlem8  29040  vtxval  29069  iedgval  29070  edgval  29118  vtxdgop  29539  finsumvtxdg2size  29619  lp1cycl  30222  ex-ind-dvds  30531  vsfval  30704  lnocoi  30828  nmblolbii  30870  ipasslem5  30906  hvsubid  31097  sshjval3  31425  pjhthlem1  31462  adjval  31961  unopf1o  31987  kbpj  32027  lnopmi  32071  nmcoplbi  32099  cnlnadjlem2  32139  adjadd  32164  branmfn  32176  pjtoi  32250  fconst7v  32693  ofoprabco  32737  supppreima  32764  sgnval2  32808  hashxpe  32880  ccatws1f1o  33011  splfv3  33018  xrsmulgzz  33069  mndractfo  33089  mndlactf1o  33090  mndractf1o  33091  gsumfs2d  33122  psgnfzto1stlem  33161  cycpmco2lem5  33191  cycpmco2lem6  33192  cyc3co2  33201  tocyccntz  33205  cyc3genpmlem  33212  cyc3conja  33218  archiabllem1a  33252  gsumvsca1  33287  gsumvsca2  33288  elrgspnlem2  33304  elrgspnsubrunlem1  33308  rloccring  33331  imaslmod  33413  elrspunidl  33488  mxidlirredi  33531  opprabs  33542  qsdrngi  33555  1arithidomlem1  33595  1arithidomlem2  33596  zringfrac  33614  ressply1evls1  33625  deg1prod  33643  psrbasfsupp  33672  mplvrpmga  33689  esplyind  33719  vietalem  33723  vieta  33724  ply1degltdimlem  33766  fedgmullem1  33773  fldextrspunlsplem  33817  extdgfialglem2  33837  algextdeglem4  33864  constrconj  33889  constrdircl  33909  constrremulcl  33911  constrimcl  33914  constrresqrtcl  33921  cos9thpiminplylem2  33927  submat1n  33949  submatres  33950  madjusmdetlem3  33973  xrge0iifhom  34081  qqhval2lem  34125  qqhrhm  34133  qqhucn  34136  esumsnf  34208  measvunilem0  34357  carsgclctunlem1  34461  ballotlemfp1  34636  ballotlemsf1o  34658  signstfveq0  34721  breprexplemc  34776  breprexp  34777  breprexpnat  34778  circlemeth  34784  logdivsqrle  34794  hgt750lema  34801  revwlk  35307  cvmlift3lem2  35502  cvmlift3lem4  35504  cvmlift3lem5  35505  cvmlift3lem6  35506  cvmlift3lem9  35509  elmrsubrn  35702  bccolsum  35921  bj-bary1lem  37624  qdiff  37641  finixpnum  37926  poimirlem4  37945  poimirlem16  37957  poimirlem19  37960  poimirlem25  37966  mblfinlem3  37980  dvtan  37991  itg2addnc  37995  itgaddnclem2  38000  ftc1anclem6  38019  areacirclem5  38033  areacirc  38034  upixp  38050  prdsbnd2  38116  ismrer1  38159  rngoneglmul  38264  rngoisocnv  38302  ecun  38714  islshpsm  39426  lshpnel2N  39431  lfl0f  39515  ldualvsdi1  39589  ldualgrplem  39591  cmtcomlemN  39694  cvlsupr8  39795  pmodl42N  40297  pmapjat1  40299  llnmod2i2  40309  dalawlem2  40318  pmapj2N  40375  idltrn  40596  cdlemc6  40642  cdleme20d  40758  cdleme22e  40790  cdleme22eALTN  40791  cdleme35b  40896  cdleme48fvg  40946  cdlemg4d  41059  cdlemg8a  41073  cdlemg42  41175  cdlemg47a  41180  tendodi1  41230  tendodi2  41231  cdlemk4  41280  cdlemk21N  41319  cdlemk22  41339  cdlemky  41372  cdlemk53b  41402  cdlemk53  41403  cdlemkyyN  41408  erngdvlem3-rN  41444  tendocnv  41467  dia1dim2  41508  dicvaddcl  41636  dihglblem3N  41741  dihmeetlem4preN  41752  dihmeet2  41792  lcfl7lem  41945  baerlem3lem1  42153  baerlem5alem1  42154  mapdh6bN  42183  mapdh6cN  42184  mapdh6dN  42185  hdmap1l6b  42257  hdmap1l6c  42258  hdmap1l6d  42259  hdmap14lem13  42326  ofun  42677  rediv23d  42893  grpcominv1  42953  evlselv  43020  flt4lem7  43092  3cubeslem2  43117  3cubeslem3r  43119  3cubeslem4  43121  pellexlem2  43258  rmxyneg  43348  oddcomabszz  43372  acongeq  43411  hausgraph  43633  onsupnmax  43656  tfsconcatrev  43776  naddass1  43821  fsovrfovd  44436  inductionexd  44582  expgrowth  44762  binomcxplemwb  44775  binomcxplemnn0  44776  binomcxplemnotnn0  44783  sumsnd  45457  restuni4  45551  fmuldfeqlem1  46012  cncfmptss  46017  climexp  46035  dvresntr  46346  stoweidlem17  46445  wallispi  46498  dirkertrigeq  46529  dirkercncflem2  46532  fourierdlem30  46565  fourierdlem41  46576  fourierdlem81  46615  fourierdlem103  46637  sge0xp  46857  sge0isummpt2  46860  isomennd  46959  vonioolem1  47108  sigarperm  47288  sin3t  47319  sin5tlem5  47325  fcores  47515  imasetpreimafvbijlemfo  47865  fundcmpsurbijinjpreimafv  47867  fundcmpsurinjimaid  47871  prprspr2  47978  ppivalnn  48095  opoeALTV  48159  uhgrimisgrgric  48407  isubgr3stgrlem2  48443  cznrng  48737  rngchomrnghmresALTV  48755  fdmdifeqresdif  48818  lincsum  48905  lincscm  48906  lmod1lem4  48966  blennngt2o2  49068  blennn0e2  49070  tposideq  49363  topdlat  49479  sectpropdlem  49511  invpropdlem  49513  isopropdlem  49515  imaidfu  49585  imasubc  49626  natoppf  49704  swapfid  49754  swapfcoa  49756  fucoppcid  49883  fucoppcco  49884  oppfdiag1  49889  diag1f1olem  50008  oppgoppchom  50065  oppgoppcco  50066  oppgoppcid  50067  2arwcat  50075  reccot  50233  rectan  50234  cotsqcscsq  50237  amgmlemALT  50278