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 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 2708

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

This theorem is referenced by:  csbun  4393  csbdif  4478  csbcnvgALT  5833  csbres  5941  fimacnvinrn2  7017  f1ossf1o  7073  suppvalbr  8106  odi  8506  phplem2  9129  cantnfp1lem3  9589  cantnfp1  9590  cardidm  9871  ackbij2lem2  10149  ackbij2lem3  10150  divneg  11833  xadddilem  13209  xadddi2  13212  dfceil2  13759  modlt  13800  modmulnn  13809  seqcaopr3  13960  bcval5  14241  hashgadd  14300  hashun3  14307  hashmap  14358  seqcoll  14387  revccat  14689  cshwmodn  14718  2cshwcom  14739  cshimadifsn0  14753  revco  14757  cshco  14759  ofccat  14892  relexpsucl  14954  dfrtrclrec2  14981  cjreb  15046  recj  15047  imcj  15055  imval2  15074  sqrtmul  15182  absmax  15253  amgm2  15293  summolem2a  15638  fsumf1o  15646  sumsnf  15666  sumsplit  15691  fsummulc2  15707  binom  15753  bcxmas  15758  incexclem  15759  incexc  15760  expcnv  15787  pwdif  15791  cvgrat  15806  prodmolem3  15856  prodmolem2a  15857  fprodf1o  15869  prodsn  15885  prodsnf  15887  fprodabs  15897  binomfallfac  15964  fallfacval4  15966  bcfallfac  15967  ege2le3  16013  efaddlem  16016  eftlub  16034  tanval3  16059  tanneg  16073  cosmul  16098  cos01bnd  16111  demoivreALT  16126  flodddiv4  16342  absmulgcd  16476  nn0expgcd  16491  lcmfunsnlem2  16567  eulerthlem2  16709  phisum  16718  pythagtriplem14  16756  pythagtriplem19  16761  pcmul  16779  pcfac  16827  prmreclem6  16849  4sqlem12  16884  vdwlem6  16914  oppccatid  17642  curf2ndf  18170  oppcyon  18192  joincomALT  18322  meetcomALT  18324  pwsco1mhm  18757  sgrp2nmndlem4  18853  qusgrp2  18988  mulgnngsum  19009  mulgnn0p1  19015  mulgneg  19022  mulgnn0dir  19034  qusghm  19184  gaid  19228  symgval  19300  pmtrdifellem3  19407  psgnunilem2  19424  odmulg  19485  sylow1lem2  19528  sylow2a  19548  sylow3lem1  19556  efgredleme  19672  efgcpbllemb  19684  gsumzaddlem  19850  gsumconst  19863  gsumzmhm  19866  ablsimpgfindlem1  20038  srgpcomp  20153  srgbinom  20166  rdivmuldivd  20349  c0mgm  20395  c0mhm  20396  zrrnghm  20469  imadrhmcl  20730  lmodvsmmulgdi  20848  lmodsubdi  20870  rmodislmodlem  20880  0lmhm  20992  lspsneq  21077  qusrhm  21231  quscrng  21238  zringlpirlem3  21419  mulgrhm  21432  phssip  21613  frlmip  21733  frlmphl  21736  asclmulg  21858  resspsrmul  21931  evlsscasrng  22060  psdadd  22106  psdvsca  22107  psdmul  22109  psdpw  22113  psropprmul  22178  evls1scasrng  22283  mat1ghm  22427  mat1mhm  22428  1marepvmarrepid  22519  mdetrlin  22546  mdetrsca2  22548  mdetunilem7  22562  mdetunilem9  22564  mndifsplit  22580  maducoeval2  22584  smadiadetglem2  22616  decpmatmul  22716  pm2mpghm  22760  pm2mpmhmlem2  22763  cpmidgsum2  22823  ptbasfi  23525  ptuni  23538  alexsubALTlem3  23993  subgtgp  24049  tsmsxplem1  24097  xmsusp  24513  restmetu  24514  nminv  24565  nrginvrcnlem  24635  copco  24974  pcoass  24980  pi1bas  24994  pi1xfrf  25009  pi1xfr  25011  isclmp  25053  cph2subdi  25166  cphassr  25168  tcphcphlem1  25191  cphipval  25199  rrxip  25346  rrxnm  25347  pjthlem1  25393  ovolunlem1a  25453  ovolfs2  25528  uniiccdif  25535  ismbf  25585  itgaddlem2  25781  ditgswap  25816  ply1divex  26098  plyeq0lem  26171  plymullem1  26175  dgrcolem1  26235  dgrcolem2  26236  vieta1lem2  26275  elqaalem2  26284  elqaalem3  26285  aaliou3lem7  26313  ulmshft  26355  mulcxplem  26649  cxpmul2  26654  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  26952  igamlgam  27016  lgam1  27030  basellem9  27055  ppifl  27126  mumul  27147  sgmmul  27168  chtublem  27178  chpub  27187  logfacrlim  27191  dchrsum2  27235  sumdchr2  27237  bposlem9  27259  lgsdir2  27297  lgsdir  27299  lgsdi  27301  lgsdirnn0  27311  lgsdinn0  27312  lgsquad3  27354  2sqblem  27398  chpo1ub  27447  dchrmusum2  27461  dchrvmasumlem1  27462  dchrvmasum2if  27464  dchrisum0fmul  27473  rpvmasum2  27479  mulog2sumlem1  27501  vmalogdivsum2  27505  log2sumbnd  27511  selberg3lem1  27524  selberg4lem1  27527  pntrsumo1  27532  selbergr  27535  pntpbnd1  27553  pntlemk  27573  lesubsd  28092  mulsunif2lem  28165  divsasswd  28199  absmuls  28240  eucliddivs  28372  zcuts  28403  expsp1  28425  expadds  28431  pw2divsrecd  28443  pw2cut2  28458  bdayfinbndlem1  28463  tgbtwnconn1lem3  28646  mideulem2  28806  axlowdimlem16  29030  axcontlem8  29044  vtxval  29073  iedgval  29074  edgval  29122  vtxdgop  29544  finsumvtxdg2size  29624  lp1cycl  30227  ex-ind-dvds  30536  vsfval  30708  lnocoi  30832  nmblolbii  30874  ipasslem5  30910  hvsubid  31101  sshjval3  31429  pjhthlem1  31466  adjval  31965  unopf1o  31991  kbpj  32031  lnopmi  32075  nmcoplbi  32103  cnlnadjlem2  32143  adjadd  32168  branmfn  32180  pjtoi  32254  fconst7v  32698  ofoprabco  32742  supppreima  32770  sgnval2  32814  hashxpe  32887  ccatws1f1o  33033  splfv3  33040  xrsmulgzz  33091  mndractfo  33111  mndlactf1o  33112  mndractf1o  33113  gsumfs2d  33144  psgnfzto1stlem  33182  cycpmco2lem5  33212  cycpmco2lem6  33213  cyc3co2  33222  tocyccntz  33226  cyc3genpmlem  33233  cyc3conja  33239  archiabllem1a  33273  gsumvsca1  33308  gsumvsca2  33309  elrgspnlem2  33325  elrgspnsubrunlem1  33329  rloccring  33352  imaslmod  33434  elrspunidl  33509  mxidlirredi  33552  opprabs  33563  qsdrngi  33576  1arithidomlem1  33616  1arithidomlem2  33617  zringfrac  33635  ressply1evls1  33646  deg1prod  33664  psrbasfsupp  33693  mplvrpmga  33710  esplyind  33731  vietalem  33735  vieta  33736  ply1degltdimlem  33779  fedgmullem1  33786  fldextrspunlsplem  33830  extdgfialglem2  33850  algextdeglem4  33877  constrconj  33902  constrdircl  33922  constrremulcl  33924  constrimcl  33927  constrresqrtcl  33934  cos9thpiminplylem2  33940  submat1n  33962  submatres  33963  madjusmdetlem3  33986  xrge0iifhom  34094  qqhval2lem  34138  qqhrhm  34146  qqhucn  34149  esumsnf  34221  measvunilem0  34370  carsgclctunlem1  34474  ballotlemfp1  34649  ballotlemsf1o  34671  signstfveq0  34734  breprexplemc  34789  breprexp  34790  breprexpnat  34791  circlemeth  34797  logdivsqrle  34807  hgt750lema  34814  revwlk  35319  cvmlift3lem2  35514  cvmlift3lem4  35516  cvmlift3lem5  35517  cvmlift3lem6  35518  cvmlift3lem9  35521  elmrsubrn  35714  bccolsum  35933  bj-bary1lem  37515  finixpnum  37806  poimirlem4  37825  poimirlem16  37837  poimirlem19  37840  poimirlem25  37846  mblfinlem3  37860  dvtan  37871  itg2addnc  37875  itgaddnclem2  37880  ftc1anclem6  37899  areacirclem5  37913  areacirc  37914  upixp  37930  prdsbnd2  37996  ismrer1  38039  rngoneglmul  38144  rngoisocnv  38182  ecun  38588  islshpsm  39250  lshpnel2N  39255  lfl0f  39339  ldualvsdi1  39413  ldualgrplem  39415  cmtcomlemN  39518  cvlsupr8  39619  pmodl42N  40121  pmapjat1  40123  llnmod2i2  40133  dalawlem2  40142  pmapj2N  40199  idltrn  40420  cdlemc6  40466  cdleme20d  40582  cdleme22e  40614  cdleme22eALTN  40615  cdleme35b  40720  cdleme48fvg  40770  cdlemg4d  40883  cdlemg8a  40897  cdlemg42  40999  cdlemg47a  41004  tendodi1  41054  tendodi2  41055  cdlemk4  41104  cdlemk21N  41143  cdlemk22  41163  cdlemky  41196  cdlemk53b  41226  cdlemk53  41227  cdlemkyyN  41232  erngdvlem3-rN  41268  tendocnv  41291  dia1dim2  41332  dicvaddcl  41460  dihglblem3N  41565  dihmeetlem4preN  41576  dihmeet2  41616  lcfl7lem  41769  baerlem3lem1  41977  baerlem5alem1  41978  mapdh6bN  42007  mapdh6cN  42008  mapdh6dN  42009  hdmap1l6b  42081  hdmap1l6c  42082  hdmap1l6d  42083  hdmap14lem13  42150  ofun  42502  grpcominv1  42773  evlselv  42840  flt4lem7  42912  3cubeslem2  42937  3cubeslem3r  42939  3cubeslem4  42941  pellexlem2  43082  rmxyneg  43172  oddcomabszz  43196  acongeq  43235  hausgraph  43457  onsupnmax  43480  tfsconcatrev  43600  naddass1  43645  fsovrfovd  44260  inductionexd  44406  expgrowth  44586  binomcxplemwb  44599  binomcxplemnn0  44600  binomcxplemnotnn0  44607  sumsnd  45281  restuni4  45375  fmuldfeqlem1  45838  cncfmptss  45843  climexp  45861  dvresntr  46172  stoweidlem17  46271  wallispi  46324  dirkertrigeq  46355  dirkercncflem2  46358  fourierdlem30  46391  fourierdlem41  46402  fourierdlem81  46441  fourierdlem103  46463  sge0xp  46683  sge0isummpt2  46686  isomennd  46785  vonioolem1  46934  sigarperm  47114  fcores  47323  imasetpreimafvbijlemfo  47661  fundcmpsurbijinjpreimafv  47663  fundcmpsurinjimaid  47667  prprspr2  47774  opoeALTV  47939  uhgrimisgrgric  48187  isubgr3stgrlem2  48223  cznrng  48517  rngchomrnghmresALTV  48535  fdmdifeqresdif  48598  lincsum  48685  lincscm  48686  lmod1lem4  48746  blennngt2o2  48848  blennn0e2  48850  tposideq  49143  topdlat  49259  sectpropdlem  49291  invpropdlem  49293  isopropdlem  49295  imaidfu  49365  imasubc  49406  natoppf  49484  swapfid  49534  swapfcoa  49536  fucoppcid  49663  fucoppcco  49664  oppfdiag1  49669  diag1f1olem  49788  oppgoppchom  49845  oppgoppcco  49846  oppgoppcid  49847  2arwcat  49855  reccot  50013  rectan  50014  cotsqcscsq  50017  amgmlemALT  50058