Theorem 3eqtr4rd 2780

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

Syntax hints:   → wi 4   = wceq 1541

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 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726

This theorem is referenced by:  csbun  4391  csbdif  4476  csbcnvgALT  5831  csbres  5939  fimacnvinrn2  7015  f1ossf1o  7071  suppvalbr  8104  odi  8504  phplem2  9127  cantnfp1lem3  9587  cantnfp1  9588  cardidm  9869  ackbij2lem2  10147  ackbij2lem3  10148  divneg  11831  xadddilem  13207  xadddi2  13210  dfceil2  13757  modlt  13798  modmulnn  13807  seqcaopr3  13958  bcval5  14239  hashgadd  14298  hashun3  14305  hashmap  14356  seqcoll  14385  revccat  14687  cshwmodn  14716  2cshwcom  14737  cshimadifsn0  14751  revco  14755  cshco  14757  ofccat  14890  relexpsucl  14952  dfrtrclrec2  14979  cjreb  15044  recj  15045  imcj  15053  imval2  15072  sqrtmul  15180  absmax  15251  amgm2  15291  summolem2a  15636  fsumf1o  15644  sumsnf  15664  sumsplit  15689  fsummulc2  15705  binom  15751  bcxmas  15756  incexclem  15757  incexc  15758  expcnv  15785  pwdif  15789  cvgrat  15804  prodmolem3  15854  prodmolem2a  15855  fprodf1o  15867  prodsn  15883  prodsnf  15885  fprodabs  15895  binomfallfac  15962  fallfacval4  15964  bcfallfac  15965  ege2le3  16011  efaddlem  16014  eftlub  16032  tanval3  16057  tanneg  16071  cosmul  16096  cos01bnd  16109  demoivreALT  16124  flodddiv4  16340  absmulgcd  16474  nn0expgcd  16489  lcmfunsnlem2  16565  eulerthlem2  16707  phisum  16716  pythagtriplem14  16754  pythagtriplem19  16759  pcmul  16777  pcfac  16825  prmreclem6  16847  4sqlem12  16882  vdwlem6  16912  oppccatid  17640  curf2ndf  18168  oppcyon  18190  joincomALT  18320  meetcomALT  18322  pwsco1mhm  18755  sgrp2nmndlem4  18851  qusgrp2  18986  mulgnngsum  19007  mulgnn0p1  19013  mulgneg  19020  mulgnn0dir  19032  qusghm  19182  gaid  19226  symgval  19298  pmtrdifellem3  19405  psgnunilem2  19422  odmulg  19483  sylow1lem2  19526  sylow2a  19546  sylow3lem1  19554  efgredleme  19670  efgcpbllemb  19682  gsumzaddlem  19848  gsumconst  19861  gsumzmhm  19864  ablsimpgfindlem1  20036  srgpcomp  20151  srgbinom  20164  rdivmuldivd  20347  c0mgm  20393  c0mhm  20394  zrrnghm  20467  imadrhmcl  20728  lmodvsmmulgdi  20846  lmodsubdi  20868  rmodislmodlem  20878  0lmhm  20990  lspsneq  21075  qusrhm  21229  quscrng  21236  zringlpirlem3  21417  mulgrhm  21430  phssip  21611  frlmip  21731  frlmphl  21734  asclmulg  21856  resspsrmul  21929  evlsscasrng  22058  psdadd  22104  psdvsca  22105  psdmul  22107  psdpw  22111  psropprmul  22176  evls1scasrng  22281  mat1ghm  22425  mat1mhm  22426  1marepvmarrepid  22517  mdetrlin  22544  mdetrsca2  22546  mdetunilem7  22560  mdetunilem9  22562  mndifsplit  22578  maducoeval2  22582  smadiadetglem2  22614  decpmatmul  22714  pm2mpghm  22758  pm2mpmhmlem2  22761  cpmidgsum2  22821  ptbasfi  23523  ptuni  23536  alexsubALTlem3  23991  subgtgp  24047  tsmsxplem1  24095  xmsusp  24511  restmetu  24512  nminv  24563  nrginvrcnlem  24633  copco  24972  pcoass  24978  pi1bas  24992  pi1xfrf  25007  pi1xfr  25009  isclmp  25051  cph2subdi  25164  cphassr  25166  tcphcphlem1  25189  cphipval  25197  rrxip  25344  rrxnm  25345  pjthlem1  25391  ovolunlem1a  25451  ovolfs2  25526  uniiccdif  25533  ismbf  25583  itgaddlem2  25779  ditgswap  25814  ply1divex  26096  plyeq0lem  26169  plymullem1  26173  dgrcolem1  26233  dgrcolem2  26234  vieta1lem2  26273  elqaalem2  26282  elqaalem3  26283  aaliou3lem7  26311  ulmshft  26353  mulcxplem  26647  cxpmul2  26652  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  26950  igamlgam  27014  lgam1  27028  basellem9  27053  ppifl  27124  mumul  27145  sgmmul  27166  chtublem  27176  chpub  27185  logfacrlim  27189  dchrsum2  27233  sumdchr2  27235  bposlem9  27257  lgsdir2  27295  lgsdir  27297  lgsdi  27299  lgsdirnn0  27309  lgsdinn0  27310  lgsquad3  27352  2sqblem  27396  chpo1ub  27445  dchrmusum2  27459  dchrvmasumlem1  27460  dchrvmasum2if  27462  dchrisum0fmul  27471  rpvmasum2  27477  mulog2sumlem1  27499  vmalogdivsum2  27503  log2sumbnd  27509  selberg3lem1  27522  selberg4lem1  27525  pntrsumo1  27530  selbergr  27533  pntpbnd1  27551  pntlemk  27571  slesubd  28065  mulsunif2lem  28138  divsasswd  28172  absmuls  28212  eucliddivs  28334  zscut  28365  expsp1  28387  expadds  28393  pw2divsrecd  28405  pw2cut2  28419  tgbtwnconn1lem3  28595  mideulem2  28755  axlowdimlem16  28979  axcontlem8  28993  vtxval  29022  iedgval  29023  edgval  29071  vtxdgop  29493  finsumvtxdg2size  29573  lp1cycl  30176  ex-ind-dvds  30485  vsfval  30657  lnocoi  30781  nmblolbii  30823  ipasslem5  30859  hvsubid  31050  sshjval3  31378  pjhthlem1  31415  adjval  31914  unopf1o  31940  kbpj  31980  lnopmi  32024  nmcoplbi  32052  cnlnadjlem2  32092  adjadd  32117  branmfn  32129  pjtoi  32203  fconst7v  32647  ofoprabco  32691  supppreima  32719  sgnval2  32763  hashxpe  32836  ccatws1f1o  32982  splfv3  32989  xrsmulgzz  33040  mndractfo  33060  mndlactf1o  33061  mndractf1o  33062  gsumfs2d  33093  psgnfzto1stlem  33131  cycpmco2lem5  33161  cycpmco2lem6  33162  cyc3co2  33171  tocyccntz  33175  cyc3genpmlem  33182  cyc3conja  33188  archiabllem1a  33222  gsumvsca1  33257  gsumvsca2  33258  elrgspnlem2  33274  elrgspnsubrunlem1  33278  rloccring  33301  imaslmod  33383  elrspunidl  33458  mxidlirredi  33501  opprabs  33512  qsdrngi  33525  1arithidomlem1  33565  1arithidomlem2  33566  zringfrac  33584  ressply1evls1  33595  deg1prod  33613  psrbasfsupp  33642  mplvrpmga  33659  esplyind  33680  vietalem  33684  vieta  33685  ply1degltdimlem  33728  fedgmullem1  33735  fldextrspunlsplem  33779  extdgfialglem2  33799  algextdeglem4  33826  constrconj  33851  constrdircl  33871  constrremulcl  33873  constrimcl  33876  constrresqrtcl  33883  cos9thpiminplylem2  33889  submat1n  33911  submatres  33912  madjusmdetlem3  33935  xrge0iifhom  34043  qqhval2lem  34087  qqhrhm  34095  qqhucn  34098  esumsnf  34170  measvunilem0  34319  carsgclctunlem1  34423  ballotlemfp1  34598  ballotlemsf1o  34620  signstfveq0  34683  breprexplemc  34738  breprexp  34739  breprexpnat  34740  circlemeth  34746  logdivsqrle  34756  hgt750lema  34763  revwlk  35268  cvmlift3lem2  35463  cvmlift3lem4  35465  cvmlift3lem5  35466  cvmlift3lem6  35467  cvmlift3lem9  35470  elmrsubrn  35663  bccolsum  35882  bj-bary1lem  37454  finixpnum  37745  poimirlem4  37764  poimirlem16  37776  poimirlem19  37779  poimirlem25  37785  mblfinlem3  37799  dvtan  37810  itg2addnc  37814  itgaddnclem2  37819  ftc1anclem6  37838  areacirclem5  37852  areacirc  37853  upixp  37869  prdsbnd2  37935  ismrer1  37978  rngoneglmul  38083  rngoisocnv  38121  ecun  38517  islshpsm  39179  lshpnel2N  39184  lfl0f  39268  ldualvsdi1  39342  ldualgrplem  39344  cmtcomlemN  39447  cvlsupr8  39548  pmodl42N  40050  pmapjat1  40052  llnmod2i2  40062  dalawlem2  40071  pmapj2N  40128  idltrn  40349  cdlemc6  40395  cdleme20d  40511  cdleme22e  40543  cdleme22eALTN  40544  cdleme35b  40649  cdleme48fvg  40699  cdlemg4d  40812  cdlemg8a  40826  cdlemg42  40928  cdlemg47a  40933  tendodi1  40983  tendodi2  40984  cdlemk4  41033  cdlemk21N  41072  cdlemk22  41092  cdlemky  41125  cdlemk53b  41155  cdlemk53  41156  cdlemkyyN  41161  erngdvlem3-rN  41197  tendocnv  41220  dia1dim2  41261  dicvaddcl  41389  dihglblem3N  41494  dihmeetlem4preN  41505  dihmeet2  41545  lcfl7lem  41698  baerlem3lem1  41906  baerlem5alem1  41907  mapdh6bN  41936  mapdh6cN  41937  mapdh6dN  41938  hdmap1l6b  42010  hdmap1l6c  42011  hdmap1l6d  42012  hdmap14lem13  42079  ofun  42434  grpcominv1  42705  evlselv  42772  flt4lem7  42844  3cubeslem2  42869  3cubeslem3r  42871  3cubeslem4  42873  pellexlem2  43014  rmxyneg  43104  oddcomabszz  43128  acongeq  43167  hausgraph  43389  onsupnmax  43412  tfsconcatrev  43532  naddass1  43577  fsovrfovd  44192  inductionexd  44338  expgrowth  44518  binomcxplemwb  44531  binomcxplemnn0  44532  binomcxplemnotnn0  44539  sumsnd  45213  restuni4  45307  fmuldfeqlem1  45770  cncfmptss  45775  climexp  45793  dvresntr  46104  stoweidlem17  46203  wallispi  46256  dirkertrigeq  46287  dirkercncflem2  46290  fourierdlem30  46323  fourierdlem41  46334  fourierdlem81  46373  fourierdlem103  46395  sge0xp  46615  sge0isummpt2  46618  isomennd  46717  vonioolem1  46866  sigarperm  47046  fcores  47255  imasetpreimafvbijlemfo  47593  fundcmpsurbijinjpreimafv  47595  fundcmpsurinjimaid  47599  prprspr2  47706  opoeALTV  47871  uhgrimisgrgric  48119  isubgr3stgrlem2  48155  cznrng  48449  rngchomrnghmresALTV  48467  fdmdifeqresdif  48530  lincsum  48617  lincscm  48618  lmod1lem4  48678  blennngt2o2  48780  blennn0e2  48782  tposideq  49075  topdlat  49191  sectpropdlem  49223  invpropdlem  49225  isopropdlem  49227  imaidfu  49297  imasubc  49338  natoppf  49416  swapfid  49466  swapfcoa  49468  fucoppcid  49595  fucoppcco  49596  oppfdiag1  49601  diag1f1olem  49720  oppgoppchom  49777  oppgoppcco  49778  oppgoppcid  49779  2arwcat  49787  reccot  49945  rectan  49946  cotsqcscsq  49949  amgmlemALT  49990