Theorem 3eqtr4rd 2789

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

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730

This theorem is referenced by:  csbun  4372  csbdif  4458  csbcnvgALT  5793  csbres  5894  fimacnvinrn2  6950  f1ossf1o  7000  odi  8410  phplem2  8991  phplem4OLD  9003  cantnfp1lem3  9438  cantnfp1  9439  cardidm  9717  ackbij2lem2  9996  ackbij2lem3  9997  divneg  11667  xadddilem  13028  xadddi2  13031  dfceil2  13559  modlt  13600  modmulnn  13609  seqcaopr3  13758  bcval5  14032  hashgadd  14092  hashun3  14099  hashmap  14150  seqcoll  14178  revccat  14479  cshwmodn  14508  2cshwcom  14529  cshimadifsn0  14543  revco  14547  cshco  14549  ofccat  14680  relexpsucl  14742  dfrtrclrec2  14769  cjreb  14834  recj  14835  imcj  14843  imval2  14862  sqrtmul  14971  absmax  15041  amgm2  15081  summolem2a  15427  fsumf1o  15435  sumsnf  15455  sumsplit  15480  fsummulc2  15496  binom  15542  bcxmas  15547  incexclem  15548  incexc  15549  expcnv  15576  pwdif  15580  cvgrat  15595  prodmolem3  15643  prodmolem2a  15644  fprodf1o  15656  prodsn  15672  prodsnf  15674  fprodabs  15684  binomfallfac  15751  fallfacval4  15753  bcfallfac  15754  ege2le3  15799  efaddlem  15802  eftlub  15818  tanval3  15843  tanneg  15857  cosmul  15882  cos01bnd  15895  demoivreALT  15910  flodddiv4  16122  absmulgcd  16257  lcmfunsnlem2  16345  eulerthlem2  16483  phisum  16491  pythagtriplem14  16529  pythagtriplem19  16534  pcmul  16552  pcfac  16600  prmreclem6  16622  4sqlem12  16657  vdwlem6  16687  oppccatid  17430  curf2ndf  17965  oppcyon  17987  joincomALT  18119  meetcomALT  18121  pwsco1mhm  18470  sgrp2nmndlem4  18567  qusgrp2  18693  mulgnngsum  18709  mulgnn0p1  18715  mulgneg  18722  mulgnn0dir  18733  qusghm  18871  gaid  18905  symgval  18976  pmtrdifellem3  19086  psgnunilem2  19103  odmulg  19163  sylow1lem2  19204  sylow2a  19224  sylow3lem1  19232  efgredleme  19349  efgcpbllemb  19361  gsumzaddlem  19522  gsumconst  19535  gsumzmhm  19538  ablsimpgfindlem1  19710  srgpcomp  19768  srgbinom  19781  lmodvsmmulgdi  20158  lmodsubdi  20180  rmodislmodlem  20190  0lmhm  20302  lspsneq  20384  qusrhm  20508  quscrng  20511  zringlpirlem3  20686  mulgrhm  20699  phssip  20863  frlmip  20985  frlmphl  20988  resspsrmul  21186  evlsscasrng  21307  psropprmul  21409  evls1scasrng  21505  mat1ghm  21632  mat1mhm  21633  1marepvmarrepid  21724  mdetrlin  21751  mdetrsca2  21753  mdetunilem7  21767  mdetunilem9  21769  mndifsplit  21785  maducoeval2  21789  smadiadetglem2  21821  decpmatmul  21921  pm2mpghm  21965  pm2mpmhmlem2  21968  cpmidgsum2  22028  ptbasfi  22732  ptuni  22745  alexsubALTlem3  23200  subgtgp  23256  tsmsxplem1  23304  xmsusp  23725  restmetu  23726  nminv  23777  nrginvrcnlem  23855  copco  24181  pcoass  24187  pi1bas  24201  pi1xfrf  24216  pi1xfr  24218  isclmp  24260  cph2subdi  24374  cphassr  24376  tcphcphlem1  24399  cphipval  24407  rrxip  24554  rrxnm  24555  pjthlem1  24601  ovolunlem1a  24660  ovolfs2  24735  uniiccdif  24742  ismbf  24792  itgaddlem2  24988  ditgswap  25023  ply1divex  25301  plyeq0lem  25371  plymullem1  25375  dgrcolem1  25434  dgrcolem2  25435  vieta1lem2  25471  elqaalem2  25480  elqaalem3  25481  aaliou3lem7  25509  ulmshft  25549  mulcxplem  25839  cxpmul2  25844  root1eq1  25908  cxpeq  25910  logbchbase  25921  cosangneg2d  25957  isosctrlem2  25969  angpieqvdlem  25978  chordthmlem3  25984  chordthmlem4  25985  chordthmlem5  25986  quad2  25989  dcubic2  25994  cubic2  25998  quart1  26006  scvxcvx  26135  igamlgam  26199  lgam1  26213  basellem9  26238  ppifl  26309  mumul  26330  sgmmul  26349  chtublem  26359  chpub  26368  logfacrlim  26372  dchrsum2  26416  sumdchr2  26418  bposlem9  26440  lgsdir2  26478  lgsdir  26480  lgsdi  26482  lgsdirnn0  26492  lgsdinn0  26493  lgsquad3  26535  2sqblem  26579  chpo1ub  26628  dchrmusum2  26642  dchrvmasumlem1  26643  dchrvmasum2if  26645  dchrisum0fmul  26654  rpvmasum2  26660  mulog2sumlem1  26682  vmalogdivsum2  26686  log2sumbnd  26692  selberg3lem1  26705  selberg4lem1  26708  pntrsumo1  26713  selbergr  26716  pntpbnd1  26734  pntlemk  26754  tgbtwnconn1lem3  26935  mideulem2  27095  axlowdimlem16  27325  axcontlem8  27339  vtxval  27370  iedgval  27371  edgval  27419  vtxdgop  27837  finsumvtxdg2size  27917  lp1cycl  28516  ex-ind-dvds  28825  vsfval  28995  lnocoi  29119  nmblolbii  29161  ipasslem5  29197  hvsubid  29388  sshjval3  29716  pjhthlem1  29753  adjval  30252  unopf1o  30278  kbpj  30318  lnopmi  30362  nmcoplbi  30390  cnlnadjlem2  30430  adjadd  30455  branmfn  30467  pjtoi  30541  ofoprabco  31001  supppreima  31025  hashxpe  31127  splfv3  31230  xrsmulgzz  31287  psgnfzto1stlem  31367  cycpmco2lem5  31397  cycpmco2lem6  31398  cyc3co2  31407  tocyccntz  31411  cyc3genpmlem  31418  cyc3conja  31424  archiabllem1a  31445  gsumvsca1  31479  gsumvsca2  31480  rdivmuldivd  31488  imaslmod  31553  elrspunidl  31606  asclmulg  31666  fedgmullem1  31710  submat1n  31755  submatres  31756  madjusmdetlem3  31779  xrge0iifhom  31887  qqhval2lem  31931  qqhrhm  31939  qqhucn  31942  esumsnf  32032  measvunilem0  32181  carsgclctunlem1  32284  ballotlemfp1  32458  ballotlemsf1o  32480  signstfveq0  32556  breprexplemc  32612  breprexp  32613  breprexpnat  32614  circlemeth  32620  logdivsqrle  32630  hgt750lema  32637  revwlk  33086  cvmlift3lem2  33282  cvmlift3lem4  33284  cvmlift3lem5  33285  cvmlift3lem6  33286  cvmlift3lem9  33289  elmrsubrn  33482  bccolsum  33705  bj-bary1lem  35481  finixpnum  35762  poimirlem4  35781  poimirlem16  35793  poimirlem19  35796  poimirlem25  35802  mblfinlem3  35816  dvtan  35827  itg2addnc  35831  itgaddnclem2  35836  ftc1anclem6  35855  areacirclem5  35869  areacirc  35870  upixp  35887  prdsbnd2  35953  ismrer1  35996  rngoneglmul  36101  rngoisocnv  36139  islshpsm  36994  lshpnel2N  36999  lfl0f  37083  ldualvsdi1  37157  ldualgrplem  37159  cmtcomlemN  37262  cvlsupr8  37363  pmodl42N  37865  pmapjat1  37867  llnmod2i2  37877  dalawlem2  37886  pmapj2N  37943  idltrn  38164  cdlemc6  38210  cdleme20d  38326  cdleme22e  38358  cdleme22eALTN  38359  cdleme35b  38464  cdleme48fvg  38514  cdlemg4d  38627  cdlemg8a  38641  cdlemg42  38743  cdlemg47a  38748  tendodi1  38798  tendodi2  38799  cdlemk4  38848  cdlemk21N  38887  cdlemk22  38907  cdlemky  38940  cdlemk53b  38970  cdlemk53  38971  cdlemkyyN  38976  erngdvlem3-rN  39012  tendocnv  39035  dia1dim2  39076  dicvaddcl  39204  dihglblem3N  39309  dihmeetlem4preN  39320  dihmeet2  39360  lcfl7lem  39513  baerlem3lem1  39721  baerlem5alem1  39722  mapdh6bN  39751  mapdh6cN  39752  mapdh6dN  39753  hdmap1l6b  39825  hdmap1l6c  39826  hdmap1l6d  39827  hdmap14lem13  39894  ofun  40211  mhphf  40285  nn0expgcd  40335  flt4lem7  40496  3cubeslem2  40507  3cubeslem3r  40509  3cubeslem4  40511  pellexlem2  40652  rmxyneg  40742  oddcomabszz  40766  acongeq  40805  hausgraph  41037  fsovrfovd  41617  inductionexd  41765  expgrowth  41953  binomcxplemwb  41966  binomcxplemnn0  41967  binomcxplemnotnn0  41974  sumsnd  42569  restuni4  42670  fmuldfeqlem1  43123  cncfmptss  43128  climexp  43146  dvresntr  43459  stoweidlem17  43558  wallispi  43611  dirkertrigeq  43642  dirkercncflem2  43645  fourierdlem30  43678  fourierdlem41  43689  fourierdlem81  43728  fourierdlem103  43750  sge0xp  43967  sge0isummpt2  43970  isomennd  44069  vonioolem1  44218  sigarperm  44376  fcores  44561  imasetpreimafvbijlemfo  44857  fundcmpsurbijinjpreimafv  44859  fundcmpsurinjimaid  44863  prprspr2  44970  opoeALTV  45135  c0mgm  45467  c0mhm  45468  zrrnghm  45475  cznrng  45513  rngchomrnghmresALTV  45554  fdmdifeqresdif  45677  lincsum  45770  lincscm  45771  lmod1lem4  45831  blennngt2o2  45938  blennn0e2  45940  topdlat  46290  reccot  46460  rectan  46461  cotsqcscsq  46464  amgmlemALT  46507