Theorem 3eqtr4rd 2851

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

Syntax hints:   → wi 4   = wceq 1637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799

This theorem is referenced by:  csbun  4207  csbcnvgALT  5508  csbres  5600  fimacnvinrn2  6571  f1ossf1o  6618  odi  7896  phplem4  8381  cantnfp1lem3  8824  cantnfp1  8825  cardidm  9068  ackbij2lem2  9347  ackbij2lem3  9348  divneg  11004  xadddilem  12342  xadddi2  12345  dfceil2  12864  modlt  12903  modmulnn  12912  seqcaopr3  13059  bcval5  13325  hashgadd  13384  hashun3  13391  hashmap  13439  seqcoll  13465  swrdccatwrd  13692  cshwmodn  13765  2cshwcom  13786  cshimadifsn0  13800  revco  13804  cshco  13806  ofccat  13933  relexpsucl  13996  cjreb  14086  recj  14087  imcj  14095  imval2  14114  sqrtmul  14223  absmax  14292  amgm2  14332  summolem2a  14669  fsumf1o  14677  sumsnf  14696  sumsn  14698  sumsplit  14722  fsummulc2  14738  binom  14784  bcxmas  14789  incexclem  14790  incexc  14791  expcnv  14818  cvgrat  14836  prodmolem3  14884  prodmolem2a  14885  fprodf1o  14897  prodsn  14913  prodsnf  14915  fprodabs  14925  binomfallfac  14992  fallfacval4  14994  bcfallfac  14995  ege2le3  15040  efaddlem  15043  eftlub  15059  tanval3  15084  tanneg  15098  cosmul  15123  cos01bnd  15136  demoivreALT  15151  flodddiv4  15356  absmulgcd  15485  lcmfunsnlem2  15572  eulerthlem2  15704  phisum  15712  pythagtriplem14  15750  pcmul  15773  pcfac  15820  prmreclem6  15842  4sqlem12  15877  vdwlem6  15907  oppccatid  16583  curf2ndf  17092  oppcyon  17114  joincomALT  17234  meetcomALT  17236  pwsco1mhm  17575  sgrp2nmndlem4  17620  qusgrp2  17738  mulgnn0p1  17757  mulgneg  17764  mulgnn0dir  17774  qusghm  17899  gaid  17933  pmtrdifellem3  18099  psgnunilem2  18116  odmulg  18174  sylow1lem2  18215  sylow2a  18235  sylow3lem1  18243  efgredleme  18357  efgcpbllemb  18369  gsumzaddlem  18522  gsumconst  18535  gsumzmhm  18538  srgpcomp  18734  srgbinom  18747  lmodvsmmulgdi  19102  lmodsubdi  19124  rmodislmodlem  19134  0lmhm  19247  lspsneq  19329  qusrhm  19446  quscrng  19449  asclrhm  19551  resspsrmul  19626  evlsscasrng  19734  psropprmul  19816  evls1scasrng  19911  zringlpirlem3  20042  mulgrhm  20054  phssip  20213  frlmip  20327  frlmphl  20330  mat1ghm  20500  mat1mhm  20501  1marepvmarrepid  20592  mdetrlin  20619  mdetrsca2  20621  mdetunilem7  20635  mdetunilem9  20637  mndifsplit  20653  maducoeval2  20657  smadiadetglem2  20690  decpmatmul  20790  pm2mpghm  20834  pm2mpmhmlem2  20837  cpmidgsum2  20897  ptbasfi  21598  ptuni  21611  alexsubALTlem3  22066  subgtgp  22122  tsmsxplem1  22169  xmsusp  22587  restmetu  22588  nminv  22638  nrginvrcnlem  22708  copco  23030  pcoass  23036  pi1bas  23050  pi1xfrf  23065  pi1xfr  23067  isclmp  23109  cph2subdi  23222  cphassr  23224  tchcphlem1  23246  cphipval  23254  rrxip  23390  rrxnm  23391  pjthlem1  23420  ovolunlem1a  23477  ovolfs2  23552  uniiccdif  23559  ismbf  23609  itgaddlem2  23804  ditgswap  23837  ply1divex  24110  plyeq0lem  24180  plymullem1  24184  dgrcolem2  24244  vieta1lem2  24280  elqaalem2  24289  elqaalem3  24290  aaliou3lem7  24318  ulmshft  24358  mulcxplem  24644  cxpmul2  24649  root1eq1  24710  cxpeq  24712  logbchbase  24723  cosangneg2d  24751  isosctrlem2  24763  angpieqvdlem  24769  chordthmlem3  24775  chordthmlem4  24776  chordthmlem5  24777  quad2  24780  dcubic2  24785  cubic2  24789  quart1  24797  scvxcvx  24926  igamlgam  24990  lgam1  25004  basellem9  25029  ppifl  25100  mumul  25121  sgmmul  25140  chtublem  25150  chpub  25159  logfacrlim  25163  dchrsum2  25207  sumdchr2  25209  bposlem9  25231  lgsdir2  25269  lgsdir  25271  lgsdi  25273  lgsdirnn0  25283  lgsdinn0  25284  lgsquad3  25326  2sqblem  25370  chpo1ub  25383  dchrmusum2  25397  dchrvmasumlem1  25398  dchrvmasum2if  25400  dchrisum0fmul  25409  rpvmasum2  25415  mulog2sumlem1  25437  vmalogdivsum2  25441  log2sumbnd  25447  selberg3lem1  25460  selberg4lem1  25463  pntrsumo1  25468  selbergr  25471  pntpbnd1  25489  pntlemk  25509  tgbtwnconn1lem3  25683  mideulem2  25840  axlowdimlem16  26051  axcontlem8  26065  vtxval  26092  iedgval  26093  edgval  26155  vtxdgop  26594  finsumvtxdg2size  26674  clwlksfoclwwlkOLD  27237  lp1cycl  27325  ex-ind-dvds  27649  vsfval  27816  lnocoi  27940  nmblolbii  27982  ipasslem5  28018  hvsubid  28211  sshjval3  28541  pjhthlem1  28578  adjval  29077  unopf1o  29103  kbpj  29143  lnopmi  29187  nmcoplbi  29215  cnlnadjlem2  29255  adjadd  29280  branmfn  29292  pjtoi  29366  ofoprabco  29791  xrsmulgzz  30003  archiabllem1a  30070  gsumvsca1  30107  gsumvsca2  30108  rdivmuldivd  30116  psgnfzto1stlem  30175  submat1n  30196  submatres  30197  madjusmdetlem3  30220  xrge0iifhom  30308  qqhval2lem  30350  qqhrhm  30358  qqhucn  30361  esumsnf  30451  measvunilem0  30601  carsgclctunlem1  30704  ballotlemfp1  30878  ballotlemsf1o  30900  signstfveq0  30979  breprexplemc  31035  breprexp  31036  breprexpnat  31037  circlemeth  31043  logdivsqrle  31053  hgt750lema  31060  cvmlift3lem2  31625  cvmlift3lem4  31627  cvmlift3lem5  31628  cvmlift3lem6  31629  cvmlift3lem9  31632  elmrsubrn  31740  bccolsum  31947  bj-bary1lem  33477  csbdif  33488  finixpnum  33707  poimirlem4  33726  poimirlem16  33738  poimirlem19  33741  poimirlem25  33747  mblfinlem3  33761  dvtan  33772  itg2addnc  33776  itgaddnclem2  33781  ftc1anclem6  33802  areacirclem5  33816  areacirc  33817  upixp  33836  prdsbnd2  33905  ismrer1  33948  rngoneglmul  34053  rngoisocnv  34091  islshpsm  34760  lshpnel2N  34765  lfl0f  34849  ldualvsdi1  34923  ldualgrplem  34925  cmtcomlemN  35028  cvlsupr8  35129  pmodl42N  35631  pmapjat1  35633  llnmod2i2  35643  dalawlem2  35652  pmapj2N  35709  idltrn  35930  cdlemc6  35977  cdleme20d  36093  cdleme22e  36125  cdleme22eALTN  36126  cdleme35b  36231  cdleme48fvg  36281  cdlemg4d  36394  cdlemg8a  36408  cdlemg42  36510  cdlemg47a  36515  tendodi1  36565  tendodi2  36566  cdlemk4  36615  cdlemk21N  36654  cdlemk22  36674  cdlemky  36707  cdlemk53b  36737  cdlemk53  36738  cdlemkyyN  36743  erngdvlem3-rN  36779  tendocnv  36802  dia1dim2  36843  dicvaddcl  36971  dihglblem3N  37076  dihmeetlem4preN  37087  dihmeet2  37127  lcfl7lem  37280  baerlem3lem1  37488  baerlem5alem1  37489  mapdh6bN  37518  mapdh6cN  37519  mapdh6dN  37520  hdmap1l6b  37592  hdmap1l6c  37593  hdmap1l6d  37594  hdmap14lem13  37661  pellexlem2  37896  rmxyneg  37986  oddcomabszz  38010  acongeq  38051  hausgraph  38291  fsovrfovd  38803  inductionexd  38953  expgrowth  39034  binomcxplemwb  39047  binomcxplemnn0  39048  binomcxplemnotnn0  39055  sumsnd  39679  restuni4  39796  fmuldfeqlem1  40294  cncfmptss  40299  climexp  40317  dvresntr  40612  stoweidlem17  40713  wallispi  40766  dirkertrigeq  40797  dirkercncflem2  40800  fourierdlem30  40833  fourierdlem41  40844  fourierdlem81  40883  fourierdlem103  40905  sge0xp  41125  sge0isummpt2  41128  isomennd  41227  vonioolem1  41376  sigarperm  41531  pwdif  42076  opoeALTV  42169  c0mgm  42477  c0mhm  42478  zrrnghm  42485  cznrng  42523  rngchomrnghmresALTV  42564  fdmdifeqresdif  42688  lincsum  42786  lincscm  42787  lmod1lem4  42847  blennngt2o2  42954  blennn0e2  42956  reccot  43070  rectan  43071  cotsqcscsq  43074  amgmlemALT  43120