Theorem 3eqtr4rd 2783

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

Syntax hints:   → wi 4   = wceq 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  csbun  4382  csbdif  4466  csbcnvgALT  5841  csbres  5949  fimacnvinrn2  7026  f1ossf1o  7083  suppvalbr  8116  odi  8516  phplem2  9141  cantnfp1lem3  9603  cantnfp1  9604  cardidm  9885  ackbij2lem2  10163  ackbij2lem3  10164  divneg  11848  xadddilem  13248  xadddi2  13251  dfceil2  13800  modlt  13841  modmulnn  13850  seqcaopr3  14001  bcval5  14282  hashgadd  14341  hashun3  14348  hashmap  14399  seqcoll  14428  revccat  14730  cshwmodn  14759  2cshwcom  14780  cshimadifsn0  14794  revco  14798  cshco  14800  ofccat  14933  relexpsucl  14995  dfrtrclrec2  15022  cjreb  15087  recj  15088  imcj  15096  imval2  15115  sqrtmul  15223  absmax  15294  amgm2  15334  summolem2a  15679  fsumf1o  15687  sumsnf  15707  sumsplit  15732  fsummulc2  15748  binom  15797  bcxmas  15802  incexclem  15803  incexc  15804  expcnv  15831  pwdif  15835  cvgrat  15850  prodmolem3  15900  prodmolem2a  15901  fprodf1o  15913  prodsn  15929  prodsnf  15931  fprodabs  15941  binomfallfac  16008  fallfacval4  16010  bcfallfac  16011  ege2le3  16057  efaddlem  16060  eftlub  16078  tanval3  16103  tanneg  16117  cosmul  16142  cos01bnd  16155  demoivreALT  16170  flodddiv4  16386  absmulgcd  16520  nn0expgcd  16535  lcmfunsnlem2  16611  eulerthlem2  16754  phisum  16763  pythagtriplem14  16801  pythagtriplem19  16806  pcmul  16824  pcfac  16872  prmreclem6  16894  4sqlem12  16929  vdwlem6  16959  oppccatid  17687  curf2ndf  18215  oppcyon  18237  joincomALT  18367  meetcomALT  18369  pwsco1mhm  18802  sgrp2nmndlem4  18901  qusgrp2  19036  mulgnngsum  19057  mulgnn0p1  19063  mulgneg  19070  mulgnn0dir  19082  qusghm  19232  gaid  19276  symgval  19348  pmtrdifellem3  19455  psgnunilem2  19472  odmulg  19533  sylow1lem2  19576  sylow2a  19596  sylow3lem1  19604  efgredleme  19720  efgcpbllemb  19732  gsumzaddlem  19898  gsumconst  19911  gsumzmhm  19914  ablsimpgfindlem1  20086  srgpcomp  20201  srgbinom  20214  rdivmuldivd  20395  c0mgm  20441  c0mhm  20442  zrrnghm  20515  imadrhmcl  20776  lmodvsmmulgdi  20894  lmodsubdi  20916  rmodislmodlem  20926  0lmhm  21037  lspsneq  21122  qusrhm  21276  quscrng  21283  zringlpirlem3  21446  mulgrhm  21459  phssip  21640  frlmip  21760  frlmphl  21763  asclmulg  21884  resspsrmul  21956  evlsscasrng  22085  psdadd  22131  psdvsca  22132  psdmul  22134  psdpw  22138  psropprmul  22203  evls1scasrng  22306  mat1ghm  22450  mat1mhm  22451  1marepvmarrepid  22542  mdetrlin  22569  mdetrsca2  22571  mdetunilem7  22585  mdetunilem9  22587  mndifsplit  22603  maducoeval2  22607  smadiadetglem2  22639  decpmatmul  22739  pm2mpghm  22783  pm2mpmhmlem2  22786  cpmidgsum2  22846  ptbasfi  23548  ptuni  23561  alexsubALTlem3  24016  subgtgp  24072  tsmsxplem1  24120  xmsusp  24536  restmetu  24537  nminv  24588  nrginvrcnlem  24658  copco  24987  pcoass  24993  pi1bas  25007  pi1xfrf  25022  pi1xfr  25024  isclmp  25066  cph2subdi  25179  cphassr  25181  tcphcphlem1  25204  cphipval  25212  rrxip  25359  rrxnm  25360  pjthlem1  25406  ovolunlem1a  25465  ovolfs2  25540  uniiccdif  25547  ismbf  25597  itgaddlem2  25793  ditgswap  25828  ply1divex  26104  plyeq0lem  26177  plymullem1  26181  dgrcolem1  26240  dgrcolem2  26241  vieta1lem2  26279  elqaalem2  26288  elqaalem3  26289  aaliou3lem7  26317  ulmshft  26357  mulcxplem  26650  cxpmul2  26655  root1eq1  26721  cxpeq  26723  logbchbase  26737  cosangneg2d  26773  isosctrlem2  26785  angpieqvdlem  26794  chordthmlem3  26800  chordthmlem4  26801  chordthmlem5  26802  quad2  26805  dcubic2  26810  cubic2  26814  quart1  26822  scvxcvx  26951  igamlgam  27015  lgam1  27029  basellem9  27054  ppifl  27125  mumul  27146  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  lesubsd  28090  mulsunif2lem  28163  divsasswd  28197  absmuls  28238  eucliddivs  28370  zcuts  28401  expsp1  28423  expadds  28429  pw2divsrecd  28441  pw2cut2  28456  bdayfinbndlem1  28461  tgbtwnconn1lem3  28644  mideulem2  28804  axlowdimlem16  29028  axcontlem8  29042  vtxval  29071  iedgval  29072  edgval  29120  vtxdgop  29541  finsumvtxdg2size  29621  lp1cycl  30224  ex-ind-dvds  30533  vsfval  30706  lnocoi  30830  nmblolbii  30872  ipasslem5  30908  hvsubid  31099  sshjval3  31427  pjhthlem1  31464  adjval  31963  unopf1o  31989  kbpj  32029  lnopmi  32073  nmcoplbi  32101  cnlnadjlem2  32141  adjadd  32166  branmfn  32178  pjtoi  32252  fconst7v  32695  ofoprabco  32739  supppreima  32766  sgnval2  32810  hashxpe  32882  ccatws1f1o  33013  splfv3  33020  xrsmulgzz  33071  mndractfo  33091  mndlactf1o  33092  mndractf1o  33093  gsumfs2d  33124  psgnfzto1stlem  33163  cycpmco2lem5  33193  cycpmco2lem6  33194  cyc3co2  33203  tocyccntz  33207  cyc3genpmlem  33214  cyc3conja  33220  archiabllem1a  33254  gsumvsca1  33289  gsumvsca2  33290  elrgspnlem2  33306  elrgspnsubrunlem1  33310  rloccring  33333  imaslmod  33415  elrspunidl  33490  mxidlirredi  33533  opprabs  33544  qsdrngi  33557  1arithidomlem1  33597  1arithidomlem2  33598  zringfrac  33616  ressply1evls1  33627  deg1prod  33645  psrbasfsupp  33674  mplvrpmga  33691  esplyind  33721  vietalem  33725  vieta  33726  ply1degltdimlem  33768  fedgmullem1  33775  fldextrspunlsplem  33819  extdgfialglem2  33839  algextdeglem4  33866  constrconj  33891  constrdircl  33911  constrremulcl  33913  constrimcl  33916  constrresqrtcl  33923  cos9thpiminplylem2  33929  submat1n  33951  submatres  33952  madjusmdetlem3  33975  xrge0iifhom  34083  qqhval2lem  34127  qqhrhm  34135  qqhucn  34138  esumsnf  34210  measvunilem0  34359  carsgclctunlem1  34463  ballotlemfp1  34638  ballotlemsf1o  34660  signstfveq0  34723  breprexplemc  34778  breprexp  34779  breprexpnat  34780  circlemeth  34786  logdivsqrle  34796  hgt750lema  34803  revwlk  35309  cvmlift3lem2  35504  cvmlift3lem4  35506  cvmlift3lem5  35507  cvmlift3lem6  35508  cvmlift3lem9  35511  elmrsubrn  35704  bccolsum  35923  bj-bary1lem  37626  qdiff  37643  finixpnum  37928  poimirlem4  37947  poimirlem16  37959  poimirlem19  37962  poimirlem25  37968  mblfinlem3  37982  dvtan  37993  itg2addnc  37997  itgaddnclem2  38002  ftc1anclem6  38021  areacirclem5  38035  areacirc  38036  upixp  38052  prdsbnd2  38118  ismrer1  38161  rngoneglmul  38266  rngoisocnv  38304  ecun  38716  islshpsm  39428  lshpnel2N  39433  lfl0f  39517  ldualvsdi1  39591  ldualgrplem  39593  cmtcomlemN  39696  cvlsupr8  39797  pmodl42N  40299  pmapjat1  40301  llnmod2i2  40311  dalawlem2  40320  pmapj2N  40377  idltrn  40598  cdlemc6  40644  cdleme20d  40760  cdleme22e  40792  cdleme22eALTN  40793  cdleme35b  40898  cdleme48fvg  40948  cdlemg4d  41061  cdlemg8a  41075  cdlemg42  41177  cdlemg47a  41182  tendodi1  41232  tendodi2  41233  cdlemk4  41282  cdlemk21N  41321  cdlemk22  41341  cdlemky  41374  cdlemk53b  41404  cdlemk53  41405  cdlemkyyN  41410  erngdvlem3-rN  41446  tendocnv  41469  dia1dim2  41510  dicvaddcl  41638  dihglblem3N  41743  dihmeetlem4preN  41754  dihmeet2  41794  lcfl7lem  41947  baerlem3lem1  42155  baerlem5alem1  42156  mapdh6bN  42185  mapdh6cN  42186  mapdh6dN  42187  hdmap1l6b  42259  hdmap1l6c  42260  hdmap1l6d  42261  hdmap14lem13  42328  ofun  42679  rediv23d  42895  grpcominv1  42955  evlselv  43022  flt4lem7  43094  3cubeslem2  43119  3cubeslem3r  43121  3cubeslem4  43123  pellexlem2  43260  rmxyneg  43350  oddcomabszz  43374  acongeq  43413  hausgraph  43635  onsupnmax  43658  tfsconcatrev  43778  naddass1  43823  fsovrfovd  44438  inductionexd  44584  expgrowth  44764  binomcxplemwb  44777  binomcxplemnn0  44778  binomcxplemnotnn0  44785  sumsnd  45459  restuni4  45553  fmuldfeqlem1  46014  cncfmptss  46019  climexp  46037  dvresntr  46348  stoweidlem17  46447  wallispi  46500  dirkertrigeq  46531  dirkercncflem2  46534  fourierdlem30  46567  fourierdlem41  46578  fourierdlem81  46617  fourierdlem103  46639  sge0xp  46859  sge0isummpt2  46862  isomennd  46961  vonioolem1  47110  sigarperm  47290  sin3t  47321  sin5tlem5  47327  fcores  47517  imasetpreimafvbijlemfo  47867  fundcmpsurbijinjpreimafv  47869  fundcmpsurinjimaid  47873  prprspr2  47980  ppivalnn  48097  opoeALTV  48161  uhgrimisgrgric  48409  isubgr3stgrlem2  48445  cznrng  48739  rngchomrnghmresALTV  48757  fdmdifeqresdif  48820  lincsum  48907  lincscm  48908  lmod1lem4  48968  blennngt2o2  49070  blennn0e2  49072  tposideq  49365  topdlat  49481  sectpropdlem  49513  invpropdlem  49515  isopropdlem  49517  imaidfu  49587  imasubc  49628  natoppf  49706  swapfid  49756  swapfcoa  49758  fucoppcid  49885  fucoppcco  49886  oppfdiag1  49891  diag1f1olem  50010  oppgoppchom  50067  oppgoppcco  50068  oppgoppcid  50069  2arwcat  50077  reccot  50235  rectan  50236  cotsqcscsq  50239  amgmlemALT  50280