Theorem 3eqtr4rd 2781

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 2773	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
4		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
5	3, 4	eqtr4d 2773	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 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  csbun  4437  csbdif  4526  csbcnvgALT  5883  csbres  5983  fimacnvinrn2  7073  f1ossf1o  7127  suppvalbr  8152  odi  8581  phplem2  9210  phplem4OLD  9222  cantnfp1lem3  9677  cantnfp1  9678  cardidm  9956  ackbij2lem2  10237  ackbij2lem3  10238  divneg  11910  xadddilem  13277  xadddi2  13280  dfceil2  13808  modlt  13849  modmulnn  13858  seqcaopr3  14007  bcval5  14282  hashgadd  14341  hashun3  14348  hashmap  14399  seqcoll  14429  revccat  14720  cshwmodn  14749  2cshwcom  14770  cshimadifsn0  14785  revco  14789  cshco  14791  ofccat  14920  relexpsucl  14982  dfrtrclrec2  15009  cjreb  15074  recj  15075  imcj  15083  imval2  15102  sqrtmul  15210  absmax  15280  amgm2  15320  summolem2a  15665  fsumf1o  15673  sumsnf  15693  sumsplit  15718  fsummulc2  15734  binom  15780  bcxmas  15785  incexclem  15786  incexc  15787  expcnv  15814  pwdif  15818  cvgrat  15833  prodmolem3  15881  prodmolem2a  15882  fprodf1o  15894  prodsn  15910  prodsnf  15912  fprodabs  15922  binomfallfac  15989  fallfacval4  15991  bcfallfac  15992  ege2le3  16037  efaddlem  16040  eftlub  16056  tanval3  16081  tanneg  16095  cosmul  16120  cos01bnd  16133  demoivreALT  16148  flodddiv4  16360  absmulgcd  16495  lcmfunsnlem2  16581  eulerthlem2  16719  phisum  16727  pythagtriplem14  16765  pythagtriplem19  16770  pcmul  16788  pcfac  16836  prmreclem6  16858  4sqlem12  16893  vdwlem6  16923  oppccatid  17669  curf2ndf  18204  oppcyon  18226  joincomALT  18358  meetcomALT  18360  pwsco1mhm  18749  sgrp2nmndlem4  18845  qusgrp2  18977  mulgnngsum  18995  mulgnn0p1  19001  mulgneg  19008  mulgnn0dir  19020  qusghm  19169  gaid  19204  symgval  19277  pmtrdifellem3  19387  psgnunilem2  19404  odmulg  19465  sylow1lem2  19508  sylow2a  19528  sylow3lem1  19536  efgredleme  19652  efgcpbllemb  19664  gsumzaddlem  19830  gsumconst  19843  gsumzmhm  19846  ablsimpgfindlem1  20018  srgpcomp  20112  srgbinom  20125  rdivmuldivd  20304  c0mgm  20350  c0mhm  20351  zrrnghm  20425  imadrhmcl  20556  lmodvsmmulgdi  20651  lmodsubdi  20673  rmodislmodlem  20683  0lmhm  20795  lspsneq  20880  qusrhm  21024  quscrng  21029  zringlpirlem3  21235  mulgrhm  21248  phssip  21430  frlmip  21552  frlmphl  21555  resspsrmul  21756  evlsscasrng  21879  psropprmul  21980  evls1scasrng  22078  mat1ghm  22205  mat1mhm  22206  1marepvmarrepid  22297  mdetrlin  22324  mdetrsca2  22326  mdetunilem7  22340  mdetunilem9  22342  mndifsplit  22358  maducoeval2  22362  smadiadetglem2  22394  decpmatmul  22494  pm2mpghm  22538  pm2mpmhmlem2  22541  cpmidgsum2  22601  ptbasfi  23305  ptuni  23318  alexsubALTlem3  23773  subgtgp  23829  tsmsxplem1  23877  xmsusp  24298  restmetu  24299  nminv  24350  nrginvrcnlem  24428  copco  24765  pcoass  24771  pi1bas  24785  pi1xfrf  24800  pi1xfr  24802  isclmp  24844  cph2subdi  24958  cphassr  24960  tcphcphlem1  24983  cphipval  24991  rrxip  25138  rrxnm  25139  pjthlem1  25185  ovolunlem1a  25245  ovolfs2  25320  uniiccdif  25327  ismbf  25377  itgaddlem2  25573  ditgswap  25608  ply1divex  25889  plyeq0lem  25959  plymullem1  25963  dgrcolem1  26023  dgrcolem2  26024  vieta1lem2  26060  elqaalem2  26069  elqaalem3  26070  aaliou3lem7  26098  ulmshft  26138  mulcxplem  26428  cxpmul2  26433  root1eq1  26499  cxpeq  26501  logbchbase  26512  cosangneg2d  26548  isosctrlem2  26560  angpieqvdlem  26569  chordthmlem3  26575  chordthmlem4  26576  chordthmlem5  26577  quad2  26580  dcubic2  26585  cubic2  26589  quart1  26597  scvxcvx  26726  igamlgam  26790  lgam1  26804  basellem9  26829  ppifl  26900  mumul  26921  sgmmul  26940  chtublem  26950  chpub  26959  logfacrlim  26963  dchrsum2  27007  sumdchr2  27009  bposlem9  27031  lgsdir2  27069  lgsdir  27071  lgsdi  27073  lgsdirnn0  27083  lgsdinn0  27084  lgsquad3  27126  2sqblem  27170  chpo1ub  27219  dchrmusum2  27233  dchrvmasumlem1  27234  dchrvmasum2if  27236  dchrisum0fmul  27245  rpvmasum2  27251  mulog2sumlem1  27273  vmalogdivsum2  27277  log2sumbnd  27283  selberg3lem1  27296  selberg4lem1  27299  pntrsumo1  27304  selbergr  27307  pntpbnd1  27325  pntlemk  27345  divsasswd  27889  tgbtwnconn1lem3  28092  mideulem2  28252  axlowdimlem16  28482  axcontlem8  28496  vtxval  28527  iedgval  28528  edgval  28576  vtxdgop  28994  finsumvtxdg2size  29074  lp1cycl  29672  ex-ind-dvds  29981  vsfval  30153  lnocoi  30277  nmblolbii  30319  ipasslem5  30355  hvsubid  30546  sshjval3  30874  pjhthlem1  30911  adjval  31410  unopf1o  31436  kbpj  31476  lnopmi  31520  nmcoplbi  31548  cnlnadjlem2  31588  adjadd  31613  branmfn  31625  pjtoi  31699  ofoprabco  32156  supppreima  32180  hashxpe  32286  splfv3  32389  xrsmulgzz  32446  psgnfzto1stlem  32529  cycpmco2lem5  32559  cycpmco2lem6  32560  cyc3co2  32569  tocyccntz  32573  cyc3genpmlem  32580  cyc3conja  32586  archiabllem1a  32607  gsumvsca1  32641  gsumvsca2  32642  imaslmod  32738  elrspunidl  32820  mxidlirredi  32861  opprabs  32870  qsdrngi  32883  asclmulg  32909  ply1degltdimlem  32995  fedgmullem1  33002  algextdeglem4  33065  submat1n  33083  submatres  33084  madjusmdetlem3  33107  xrge0iifhom  33215  qqhval2lem  33259  qqhrhm  33267  qqhucn  33270  esumsnf  33360  measvunilem0  33509  carsgclctunlem1  33614  ballotlemfp1  33788  ballotlemsf1o  33810  signstfveq0  33886  breprexplemc  33942  breprexp  33943  breprexpnat  33944  circlemeth  33950  logdivsqrle  33960  hgt750lema  33967  revwlk  34413  cvmlift3lem2  34609  cvmlift3lem4  34611  cvmlift3lem5  34612  cvmlift3lem6  34613  cvmlift3lem9  34616  elmrsubrn  34809  bccolsum  35013  bj-bary1lem  36494  finixpnum  36776  poimirlem4  36795  poimirlem16  36807  poimirlem19  36810  poimirlem25  36816  mblfinlem3  36830  dvtan  36841  itg2addnc  36845  itgaddnclem2  36850  ftc1anclem6  36869  areacirclem5  36883  areacirc  36884  upixp  36900  prdsbnd2  36966  ismrer1  37009  rngoneglmul  37114  rngoisocnv  37152  islshpsm  38153  lshpnel2N  38158  lfl0f  38242  ldualvsdi1  38316  ldualgrplem  38318  cmtcomlemN  38421  cvlsupr8  38522  pmodl42N  39025  pmapjat1  39027  llnmod2i2  39037  dalawlem2  39046  pmapj2N  39103  idltrn  39324  cdlemc6  39370  cdleme20d  39486  cdleme22e  39518  cdleme22eALTN  39519  cdleme35b  39624  cdleme48fvg  39674  cdlemg4d  39787  cdlemg8a  39801  cdlemg42  39903  cdlemg47a  39908  tendodi1  39958  tendodi2  39959  cdlemk4  40008  cdlemk21N  40047  cdlemk22  40067  cdlemky  40100  cdlemk53b  40130  cdlemk53  40131  cdlemkyyN  40136  erngdvlem3-rN  40172  tendocnv  40195  dia1dim2  40236  dicvaddcl  40364  dihglblem3N  40469  dihmeetlem4preN  40480  dihmeet2  40520  lcfl7lem  40673  baerlem3lem1  40881  baerlem5alem1  40882  mapdh6bN  40911  mapdh6cN  40912  mapdh6dN  40913  hdmap1l6b  40985  hdmap1l6c  40986  hdmap1l6d  40987  hdmap14lem13  41054  ofun  41364  grpcominv1  41388  evlselv  41461  nn0expgcd  41528  flt4lem7  41703  3cubeslem2  41725  3cubeslem3r  41727  3cubeslem4  41729  pellexlem2  41870  rmxyneg  41961  oddcomabszz  41985  acongeq  42024  hausgraph  42256  onsupnmax  42279  tfsconcatrev  42400  naddass1  42446  fsovrfovd  43062  inductionexd  43208  expgrowth  43396  binomcxplemwb  43409  binomcxplemnn0  43410  binomcxplemnotnn0  43417  sumsnd  44012  restuni4  44111  fmuldfeqlem1  44596  cncfmptss  44601  climexp  44619  dvresntr  44932  stoweidlem17  45031  wallispi  45084  dirkertrigeq  45115  dirkercncflem2  45118  fourierdlem30  45151  fourierdlem41  45162  fourierdlem81  45201  fourierdlem103  45223  sge0xp  45443  sge0isummpt2  45446  isomennd  45545  vonioolem1  45694  sigarperm  45874  fcores  46075  imasetpreimafvbijlemfo  46371  fundcmpsurbijinjpreimafv  46373  fundcmpsurinjimaid  46377  prprspr2  46484  opoeALTV  46649  cznrng  46941  rngchomrnghmresALTV  46982  fdmdifeqresdif  47105  lincsum  47197  lincscm  47198  lmod1lem4  47258  blennngt2o2  47365  blennn0e2  47367  topdlat  47716  reccot  47890  rectan  47891  cotsqcscsq  47894  amgmlemALT  47937