Theorem 3eqtr4rd 2804

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

Syntax hints:   → wi 4   = wceq 1538

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750

This theorem is referenced by:  csbun  4335  csbcnvgALT  5724  csbres  5826  fimacnvinrn2  6832  f1ossf1o  6881  odi  8215  phplem4  8721  cantnfp1lem3  9176  cantnfp1  9177  cardidm  9421  ackbij2lem2  9700  ackbij2lem3  9701  divneg  11370  xadddilem  12728  xadddi2  12731  dfceil2  13258  modlt  13297  modmulnn  13306  seqcaopr3  13455  bcval5  13728  hashgadd  13788  hashun3  13795  hashmap  13846  seqcoll  13874  revccat  14175  cshwmodn  14204  2cshwcom  14225  cshimadifsn0  14239  revco  14243  cshco  14245  ofccat  14376  relexpsucl  14438  dfrtrclrec2  14465  cjreb  14530  recj  14531  imcj  14539  imval2  14558  sqrtmul  14667  absmax  14737  amgm2  14777  summolem2a  15120  fsumf1o  15128  sumsnf  15147  sumsplit  15171  fsummulc2  15187  binom  15233  bcxmas  15238  incexclem  15239  incexc  15240  expcnv  15267  pwdif  15271  cvgrat  15287  prodmolem3  15335  prodmolem2a  15336  fprodf1o  15348  prodsn  15364  prodsnf  15366  fprodabs  15376  binomfallfac  15443  fallfacval4  15445  bcfallfac  15446  ege2le3  15491  efaddlem  15494  eftlub  15510  tanval3  15535  tanneg  15549  cosmul  15574  cos01bnd  15587  demoivreALT  15602  flodddiv4  15814  absmulgcd  15948  lcmfunsnlem2  16036  eulerthlem2  16174  phisum  16182  pythagtriplem14  16220  pythagtriplem19  16225  pcmul  16243  pcfac  16290  prmreclem6  16312  4sqlem12  16347  vdwlem6  16377  oppccatid  17047  curf2ndf  17563  oppcyon  17585  joincomALT  17705  meetcomALT  17707  pwsco1mhm  18062  sgrp2nmndlem4  18159  qusgrp2  18284  mulgnngsum  18300  mulgnn0p1  18306  mulgneg  18313  mulgnn0dir  18324  qusghm  18462  gaid  18496  symgval  18564  pmtrdifellem3  18673  psgnunilem2  18690  odmulg  18750  sylow1lem2  18791  sylow2a  18811  sylow3lem1  18819  efgredleme  18936  efgcpbllemb  18948  gsumzaddlem  19109  gsumconst  19122  gsumzmhm  19125  ablsimpgfindlem1  19297  srgpcomp  19350  srgbinom  19363  lmodvsmmulgdi  19737  lmodsubdi  19759  rmodislmodlem  19769  0lmhm  19880  lspsneq  19962  qusrhm  20078  quscrng  20081  zringlpirlem3  20254  mulgrhm  20267  phssip  20423  frlmip  20543  frlmphl  20546  ascldimulOLD  20651  resspsrmul  20745  evlsscasrng  20860  psropprmul  20962  evls1scasrng  21058  mat1ghm  21183  mat1mhm  21184  1marepvmarrepid  21275  mdetrlin  21302  mdetrsca2  21304  mdetunilem7  21318  mdetunilem9  21320  mndifsplit  21336  maducoeval2  21340  smadiadetglem2  21372  decpmatmul  21472  pm2mpghm  21516  pm2mpmhmlem2  21519  cpmidgsum2  21579  ptbasfi  22281  ptuni  22294  alexsubALTlem3  22749  subgtgp  22805  tsmsxplem1  22853  xmsusp  23271  restmetu  23272  nminv  23323  nrginvrcnlem  23393  copco  23719  pcoass  23725  pi1bas  23739  pi1xfrf  23754  pi1xfr  23756  isclmp  23798  cph2subdi  23911  cphassr  23913  tcphcphlem1  23935  cphipval  23943  rrxip  24090  rrxnm  24091  pjthlem1  24137  ovolunlem1a  24196  ovolfs2  24271  uniiccdif  24278  ismbf  24328  itgaddlem2  24523  ditgswap  24558  ply1divex  24836  plyeq0lem  24906  plymullem1  24910  dgrcolem1  24969  dgrcolem2  24970  vieta1lem2  25006  elqaalem2  25015  elqaalem3  25016  aaliou3lem7  25044  ulmshft  25084  mulcxplem  25374  cxpmul2  25379  root1eq1  25443  cxpeq  25445  logbchbase  25456  cosangneg2d  25492  isosctrlem2  25504  angpieqvdlem  25513  chordthmlem3  25519  chordthmlem4  25520  chordthmlem5  25521  quad2  25524  dcubic2  25529  cubic2  25533  quart1  25541  scvxcvx  25670  igamlgam  25734  lgam1  25748  basellem9  25773  ppifl  25844  mumul  25865  sgmmul  25884  chtublem  25894  chpub  25903  logfacrlim  25907  dchrsum2  25951  sumdchr2  25953  bposlem9  25975  lgsdir2  26013  lgsdir  26015  lgsdi  26017  lgsdirnn0  26027  lgsdinn0  26028  lgsquad3  26070  2sqblem  26114  chpo1ub  26163  dchrmusum2  26177  dchrvmasumlem1  26178  dchrvmasum2if  26180  dchrisum0fmul  26189  rpvmasum2  26195  mulog2sumlem1  26217  vmalogdivsum2  26221  log2sumbnd  26227  selberg3lem1  26240  selberg4lem1  26243  pntrsumo1  26248  selbergr  26251  pntpbnd1  26269  pntlemk  26289  tgbtwnconn1lem3  26467  mideulem2  26627  axlowdimlem16  26850  axcontlem8  26864  vtxval  26892  iedgval  26893  edgval  26941  vtxdgop  27359  finsumvtxdg2size  27439  lp1cycl  28036  ex-ind-dvds  28345  vsfval  28515  lnocoi  28639  nmblolbii  28681  ipasslem5  28717  hvsubid  28908  sshjval3  29236  pjhthlem1  29273  adjval  29772  unopf1o  29798  kbpj  29838  lnopmi  29882  nmcoplbi  29910  cnlnadjlem2  29950  adjadd  29975  branmfn  29987  pjtoi  30061  ofoprabco  30525  supppreima  30549  hashxpe  30651  splfv3  30754  xrsmulgzz  30813  psgnfzto1stlem  30893  cycpmco2lem5  30923  cycpmco2lem6  30924  cyc3co2  30933  tocyccntz  30937  cyc3genpmlem  30944  cyc3conja  30950  archiabllem1a  30971  gsumvsca1  31005  gsumvsca2  31006  rdivmuldivd  31014  imaslmod  31074  elrspunidl  31127  asclmulg  31187  fedgmullem1  31231  submat1n  31276  submatres  31277  madjusmdetlem3  31300  xrge0iifhom  31408  qqhval2lem  31450  qqhrhm  31458  qqhucn  31461  esumsnf  31551  measvunilem0  31700  carsgclctunlem1  31803  ballotlemfp1  31977  ballotlemsf1o  31999  signstfveq0  32075  breprexplemc  32131  breprexp  32132  breprexpnat  32133  circlemeth  32139  logdivsqrle  32149  hgt750lema  32156  revwlk  32602  cvmlift3lem2  32798  cvmlift3lem4  32800  cvmlift3lem5  32801  cvmlift3lem6  32802  cvmlift3lem9  32805  elmrsubrn  32998  bccolsum  33220  bj-bary1lem  35004  csbdif  35022  finixpnum  35322  poimirlem4  35341  poimirlem16  35353  poimirlem19  35356  poimirlem25  35362  mblfinlem3  35376  dvtan  35387  itg2addnc  35391  itgaddnclem2  35396  ftc1anclem6  35415  areacirclem5  35429  areacirc  35430  upixp  35447  prdsbnd2  35513  ismrer1  35556  rngoneglmul  35661  rngoisocnv  35699  islshpsm  36556  lshpnel2N  36561  lfl0f  36645  ldualvsdi1  36719  ldualgrplem  36721  cmtcomlemN  36824  cvlsupr8  36925  pmodl42N  37427  pmapjat1  37429  llnmod2i2  37439  dalawlem2  37448  pmapj2N  37505  idltrn  37726  cdlemc6  37772  cdleme20d  37888  cdleme22e  37920  cdleme22eALTN  37921  cdleme35b  38026  cdleme48fvg  38076  cdlemg4d  38189  cdlemg8a  38203  cdlemg42  38305  cdlemg47a  38310  tendodi1  38360  tendodi2  38361  cdlemk4  38410  cdlemk21N  38449  cdlemk22  38469  cdlemky  38502  cdlemk53b  38532  cdlemk53  38533  cdlemkyyN  38538  erngdvlem3-rN  38574  tendocnv  38597  dia1dim2  38638  dicvaddcl  38766  dihglblem3N  38871  dihmeetlem4preN  38882  dihmeet2  38922  lcfl7lem  39075  baerlem3lem1  39283  baerlem5alem1  39284  mapdh6bN  39313  mapdh6cN  39314  mapdh6dN  39315  hdmap1l6b  39387  hdmap1l6c  39388  hdmap1l6d  39389  hdmap14lem13  39456  ofun  39717  mhphf  39790  nn0expgcd  39832  flt4lem7  39988  3cubeslem2  39999  3cubeslem3r  40001  3cubeslem4  40003  pellexlem2  40144  rmxyneg  40234  oddcomabszz  40258  acongeq  40297  hausgraph  40529  fsovrfovd  41083  inductionexd  41231  expgrowth  41412  binomcxplemwb  41425  binomcxplemnn0  41426  binomcxplemnotnn0  41433  sumsnd  42028  restuni4  42129  fmuldfeqlem1  42590  cncfmptss  42595  climexp  42613  dvresntr  42926  stoweidlem17  43025  wallispi  43078  dirkertrigeq  43109  dirkercncflem2  43112  fourierdlem30  43145  fourierdlem41  43156  fourierdlem81  43195  fourierdlem103  43217  sge0xp  43434  sge0isummpt2  43437  isomennd  43536  vonioolem1  43685  sigarperm  43840  imasetpreimafvbijlemfo  44290  fundcmpsurbijinjpreimafv  44292  fundcmpsurinjimaid  44296  prprspr2  44403  opoeALTV  44568  c0mgm  44900  c0mhm  44901  zrrnghm  44908  cznrng  44946  rngchomrnghmresALTV  44987  fdmdifeqresdif  45110  lincsum  45203  lincscm  45204  lmod1lem4  45264  blennngt2o2  45371  blennn0e2  45373  reccot  45675  rectan  45676  cotsqcscsq  45679  amgmlemALT  45722