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 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  csbun  4438  csbdif  4527  csbcnvgALT  5884  csbres  5984  fimacnvinrn2  7074  f1ossf1o  7128  suppvalbr  8153  odi  8582  phplem2  9211  phplem4OLD  9223  cantnfp1lem3  9678  cantnfp1  9679  cardidm  9957  ackbij2lem2  10238  ackbij2lem3  10239  divneg  11911  xadddilem  13278  xadddi2  13281  dfceil2  13809  modlt  13850  modmulnn  13859  seqcaopr3  14008  bcval5  14283  hashgadd  14342  hashun3  14349  hashmap  14400  seqcoll  14430  revccat  14721  cshwmodn  14750  2cshwcom  14771  cshimadifsn0  14786  revco  14790  cshco  14792  ofccat  14921  relexpsucl  14983  dfrtrclrec2  15010  cjreb  15075  recj  15076  imcj  15084  imval2  15103  sqrtmul  15211  absmax  15281  amgm2  15321  summolem2a  15666  fsumf1o  15674  sumsnf  15694  sumsplit  15719  fsummulc2  15735  binom  15781  bcxmas  15786  incexclem  15787  incexc  15788  expcnv  15815  pwdif  15819  cvgrat  15834  prodmolem3  15882  prodmolem2a  15883  fprodf1o  15895  prodsn  15911  prodsnf  15913  fprodabs  15923  binomfallfac  15990  fallfacval4  15992  bcfallfac  15993  ege2le3  16038  efaddlem  16041  eftlub  16057  tanval3  16082  tanneg  16096  cosmul  16121  cos01bnd  16134  demoivreALT  16149  flodddiv4  16361  absmulgcd  16496  lcmfunsnlem2  16582  eulerthlem2  16720  phisum  16728  pythagtriplem14  16766  pythagtriplem19  16771  pcmul  16789  pcfac  16837  prmreclem6  16859  4sqlem12  16894  vdwlem6  16924  oppccatid  17670  curf2ndf  18205  oppcyon  18227  joincomALT  18359  meetcomALT  18361  pwsco1mhm  18750  sgrp2nmndlem4  18846  qusgrp2  18978  mulgnngsum  18996  mulgnn0p1  19002  mulgneg  19009  mulgnn0dir  19021  qusghm  19170  gaid  19205  symgval  19278  pmtrdifellem3  19388  psgnunilem2  19405  odmulg  19466  sylow1lem2  19509  sylow2a  19529  sylow3lem1  19537  efgredleme  19653  efgcpbllemb  19665  gsumzaddlem  19831  gsumconst  19844  gsumzmhm  19847  ablsimpgfindlem1  20019  srgpcomp  20113  srgbinom  20126  rdivmuldivd  20305  c0mgm  20351  c0mhm  20352  zrrnghm  20426  imadrhmcl  20557  lmodvsmmulgdi  20652  lmodsubdi  20674  rmodislmodlem  20684  0lmhm  20796  lspsneq  20881  qusrhm  21025  quscrng  21030  zringlpirlem3  21236  mulgrhm  21249  phssip  21431  frlmip  21553  frlmphl  21556  resspsrmul  21757  evlsscasrng  21880  psropprmul  21981  evls1scasrng  22079  mat1ghm  22206  mat1mhm  22207  1marepvmarrepid  22298  mdetrlin  22325  mdetrsca2  22327  mdetunilem7  22341  mdetunilem9  22343  mndifsplit  22359  maducoeval2  22363  smadiadetglem2  22395  decpmatmul  22495  pm2mpghm  22539  pm2mpmhmlem2  22542  cpmidgsum2  22602  ptbasfi  23306  ptuni  23319  alexsubALTlem3  23774  subgtgp  23830  tsmsxplem1  23878  xmsusp  24299  restmetu  24300  nminv  24351  nrginvrcnlem  24429  copco  24766  pcoass  24772  pi1bas  24786  pi1xfrf  24801  pi1xfr  24803  isclmp  24845  cph2subdi  24959  cphassr  24961  tcphcphlem1  24984  cphipval  24992  rrxip  25139  rrxnm  25140  pjthlem1  25186  ovolunlem1a  25246  ovolfs2  25321  uniiccdif  25328  ismbf  25378  itgaddlem2  25574  ditgswap  25609  ply1divex  25890  plyeq0lem  25960  plymullem1  25964  dgrcolem1  26024  dgrcolem2  26025  vieta1lem2  26061  elqaalem2  26070  elqaalem3  26071  aaliou3lem7  26099  ulmshft  26139  mulcxplem  26429  cxpmul2  26434  root1eq1  26500  cxpeq  26502  logbchbase  26513  cosangneg2d  26549  isosctrlem2  26561  angpieqvdlem  26570  chordthmlem3  26576  chordthmlem4  26577  chordthmlem5  26578  quad2  26581  dcubic2  26586  cubic2  26590  quart1  26598  scvxcvx  26727  igamlgam  26791  lgam1  26805  basellem9  26830  ppifl  26901  mumul  26922  sgmmul  26941  chtublem  26951  chpub  26960  logfacrlim  26964  dchrsum2  27008  sumdchr2  27010  bposlem9  27032  lgsdir2  27070  lgsdir  27072  lgsdi  27074  lgsdirnn0  27084  lgsdinn0  27085  lgsquad3  27127  2sqblem  27171  chpo1ub  27220  dchrmusum2  27234  dchrvmasumlem1  27235  dchrvmasum2if  27237  dchrisum0fmul  27246  rpvmasum2  27252  mulog2sumlem1  27274  vmalogdivsum2  27278  log2sumbnd  27284  selberg3lem1  27297  selberg4lem1  27300  pntrsumo1  27305  selbergr  27308  pntpbnd1  27326  pntlemk  27346  divsasswd  27890  tgbtwnconn1lem3  28093  mideulem2  28253  axlowdimlem16  28483  axcontlem8  28497  vtxval  28528  iedgval  28529  edgval  28577  vtxdgop  28995  finsumvtxdg2size  29075  lp1cycl  29673  ex-ind-dvds  29982  vsfval  30154  lnocoi  30278  nmblolbii  30320  ipasslem5  30356  hvsubid  30547  sshjval3  30875  pjhthlem1  30912  adjval  31411  unopf1o  31437  kbpj  31477  lnopmi  31521  nmcoplbi  31549  cnlnadjlem2  31589  adjadd  31614  branmfn  31626  pjtoi  31700  ofoprabco  32157  supppreima  32181  hashxpe  32287  splfv3  32390  xrsmulgzz  32447  psgnfzto1stlem  32530  cycpmco2lem5  32560  cycpmco2lem6  32561  cyc3co2  32570  tocyccntz  32574  cyc3genpmlem  32581  cyc3conja  32587  archiabllem1a  32608  gsumvsca1  32642  gsumvsca2  32643  imaslmod  32739  elrspunidl  32821  mxidlirredi  32862  opprabs  32871  qsdrngi  32884  asclmulg  32910  ply1degltdimlem  32996  fedgmullem1  33003  algextdeglem4  33066  submat1n  33084  submatres  33085  madjusmdetlem3  33108  xrge0iifhom  33216  qqhval2lem  33260  qqhrhm  33268  qqhucn  33271  esumsnf  33361  measvunilem0  33510  carsgclctunlem1  33615  ballotlemfp1  33789  ballotlemsf1o  33811  signstfveq0  33887  breprexplemc  33943  breprexp  33944  breprexpnat  33945  circlemeth  33951  logdivsqrle  33961  hgt750lema  33968  revwlk  34414  cvmlift3lem2  34610  cvmlift3lem4  34612  cvmlift3lem5  34613  cvmlift3lem6  34614  cvmlift3lem9  34617  elmrsubrn  34810  bccolsum  35014  bj-bary1lem  36495  finixpnum  36777  poimirlem4  36796  poimirlem16  36808  poimirlem19  36811  poimirlem25  36817  mblfinlem3  36831  dvtan  36842  itg2addnc  36846  itgaddnclem2  36851  ftc1anclem6  36870  areacirclem5  36884  areacirc  36885  upixp  36901  prdsbnd2  36967  ismrer1  37010  rngoneglmul  37115  rngoisocnv  37153  islshpsm  38154  lshpnel2N  38159  lfl0f  38243  ldualvsdi1  38317  ldualgrplem  38319  cmtcomlemN  38422  cvlsupr8  38523  pmodl42N  39026  pmapjat1  39028  llnmod2i2  39038  dalawlem2  39047  pmapj2N  39104  idltrn  39325  cdlemc6  39371  cdleme20d  39487  cdleme22e  39519  cdleme22eALTN  39520  cdleme35b  39625  cdleme48fvg  39675  cdlemg4d  39788  cdlemg8a  39802  cdlemg42  39904  cdlemg47a  39909  tendodi1  39959  tendodi2  39960  cdlemk4  40009  cdlemk21N  40048  cdlemk22  40068  cdlemky  40101  cdlemk53b  40131  cdlemk53  40132  cdlemkyyN  40137  erngdvlem3-rN  40173  tendocnv  40196  dia1dim2  40237  dicvaddcl  40365  dihglblem3N  40470  dihmeetlem4preN  40481  dihmeet2  40521  lcfl7lem  40674  baerlem3lem1  40882  baerlem5alem1  40883  mapdh6bN  40912  mapdh6cN  40913  mapdh6dN  40914  hdmap1l6b  40986  hdmap1l6c  40987  hdmap1l6d  40988  hdmap14lem13  41055  ofun  41365  grpcominv1  41389  evlselv  41462  nn0expgcd  41529  flt4lem7  41704  3cubeslem2  41726  3cubeslem3r  41728  3cubeslem4  41730  pellexlem2  41871  rmxyneg  41962  oddcomabszz  41986  acongeq  42025  hausgraph  42257  onsupnmax  42280  tfsconcatrev  42401  naddass1  42447  fsovrfovd  43063  inductionexd  43209  expgrowth  43397  binomcxplemwb  43410  binomcxplemnn0  43411  binomcxplemnotnn0  43418  sumsnd  44013  restuni4  44112  fmuldfeqlem1  44597  cncfmptss  44602  climexp  44620  dvresntr  44933  stoweidlem17  45032  wallispi  45085  dirkertrigeq  45116  dirkercncflem2  45119  fourierdlem30  45152  fourierdlem41  45163  fourierdlem81  45202  fourierdlem103  45224  sge0xp  45444  sge0isummpt2  45447  isomennd  45546  vonioolem1  45695  sigarperm  45875  fcores  46076  imasetpreimafvbijlemfo  46372  fundcmpsurbijinjpreimafv  46374  fundcmpsurinjimaid  46378  prprspr2  46485  opoeALTV  46650  cznrng  46942  rngchomrnghmresALTV  46983  fdmdifeqresdif  47106  lincsum  47198  lincscm  47199  lmod1lem4  47259  blennngt2o2  47366  blennn0e2  47368  topdlat  47717  reccot  47891  rectan  47892  cotsqcscsq  47895  amgmlemALT  47938