Theorem 3eqtr4rd 2777

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 2769	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
4		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
5	3, 4	eqtr4d 2769	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 2121  ax-ext 2703

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

This theorem is referenced by:  csbun  4388  csbdif  4471  csbcnvgALT  5823  csbres  5930  fimacnvinrn2  7005  f1ossf1o  7061  suppvalbr  8094  odi  8494  phplem2  9114  cantnfp1lem3  9570  cantnfp1  9571  cardidm  9852  ackbij2lem2  10130  ackbij2lem3  10131  divneg  11813  xadddilem  13193  xadddi2  13196  dfceil2  13743  modlt  13784  modmulnn  13793  seqcaopr3  13944  bcval5  14225  hashgadd  14284  hashun3  14291  hashmap  14342  seqcoll  14371  revccat  14673  cshwmodn  14702  2cshwcom  14723  cshimadifsn0  14737  revco  14741  cshco  14743  ofccat  14876  relexpsucl  14938  dfrtrclrec2  14965  cjreb  15030  recj  15031  imcj  15039  imval2  15058  sqrtmul  15166  absmax  15237  amgm2  15277  summolem2a  15622  fsumf1o  15630  sumsnf  15650  sumsplit  15675  fsummulc2  15691  binom  15737  bcxmas  15742  incexclem  15743  incexc  15744  expcnv  15771  pwdif  15775  cvgrat  15790  prodmolem3  15840  prodmolem2a  15841  fprodf1o  15853  prodsn  15869  prodsnf  15871  fprodabs  15881  binomfallfac  15948  fallfacval4  15950  bcfallfac  15951  ege2le3  15997  efaddlem  16000  eftlub  16018  tanval3  16043  tanneg  16057  cosmul  16082  cos01bnd  16095  demoivreALT  16110  flodddiv4  16326  absmulgcd  16460  nn0expgcd  16475  lcmfunsnlem2  16551  eulerthlem2  16693  phisum  16702  pythagtriplem14  16740  pythagtriplem19  16745  pcmul  16763  pcfac  16811  prmreclem6  16833  4sqlem12  16868  vdwlem6  16898  oppccatid  17625  curf2ndf  18153  oppcyon  18175  joincomALT  18305  meetcomALT  18307  pwsco1mhm  18740  sgrp2nmndlem4  18836  qusgrp2  18971  mulgnngsum  18992  mulgnn0p1  18998  mulgneg  19005  mulgnn0dir  19017  qusghm  19167  gaid  19211  symgval  19283  pmtrdifellem3  19390  psgnunilem2  19407  odmulg  19468  sylow1lem2  19511  sylow2a  19531  sylow3lem1  19539  efgredleme  19655  efgcpbllemb  19667  gsumzaddlem  19833  gsumconst  19846  gsumzmhm  19849  ablsimpgfindlem1  20021  srgpcomp  20136  srgbinom  20149  rdivmuldivd  20331  c0mgm  20377  c0mhm  20378  zrrnghm  20451  imadrhmcl  20712  lmodvsmmulgdi  20830  lmodsubdi  20852  rmodislmodlem  20862  0lmhm  20974  lspsneq  21059  qusrhm  21213  quscrng  21220  zringlpirlem3  21401  mulgrhm  21414  phssip  21595  frlmip  21715  frlmphl  21718  asclmulg  21839  resspsrmul  21913  evlsscasrng  22032  psdadd  22078  psdvsca  22079  psdmul  22081  psdpw  22085  psropprmul  22150  evls1scasrng  22254  mat1ghm  22398  mat1mhm  22399  1marepvmarrepid  22490  mdetrlin  22517  mdetrsca2  22519  mdetunilem7  22533  mdetunilem9  22535  mndifsplit  22551  maducoeval2  22555  smadiadetglem2  22587  decpmatmul  22687  pm2mpghm  22731  pm2mpmhmlem2  22734  cpmidgsum2  22794  ptbasfi  23496  ptuni  23509  alexsubALTlem3  23964  subgtgp  24020  tsmsxplem1  24068  xmsusp  24484  restmetu  24485  nminv  24536  nrginvrcnlem  24606  copco  24945  pcoass  24951  pi1bas  24965  pi1xfrf  24980  pi1xfr  24982  isclmp  25024  cph2subdi  25137  cphassr  25139  tcphcphlem1  25162  cphipval  25170  rrxip  25317  rrxnm  25318  pjthlem1  25364  ovolunlem1a  25424  ovolfs2  25499  uniiccdif  25506  ismbf  25556  itgaddlem2  25752  ditgswap  25787  ply1divex  26069  plyeq0lem  26142  plymullem1  26146  dgrcolem1  26206  dgrcolem2  26207  vieta1lem2  26246  elqaalem2  26255  elqaalem3  26256  aaliou3lem7  26284  ulmshft  26326  mulcxplem  26620  cxpmul2  26625  root1eq1  26692  cxpeq  26694  logbchbase  26708  cosangneg2d  26744  isosctrlem2  26756  angpieqvdlem  26765  chordthmlem3  26771  chordthmlem4  26772  chordthmlem5  26773  quad2  26776  dcubic2  26781  cubic2  26785  quart1  26793  scvxcvx  26923  igamlgam  26987  lgam1  27001  basellem9  27026  ppifl  27097  mumul  27118  sgmmul  27139  chtublem  27149  chpub  27158  logfacrlim  27162  dchrsum2  27206  sumdchr2  27208  bposlem9  27230  lgsdir2  27268  lgsdir  27270  lgsdi  27272  lgsdirnn0  27282  lgsdinn0  27283  lgsquad3  27325  2sqblem  27369  chpo1ub  27418  dchrmusum2  27432  dchrvmasumlem1  27433  dchrvmasum2if  27435  dchrisum0fmul  27444  rpvmasum2  27450  mulog2sumlem1  27472  vmalogdivsum2  27476  log2sumbnd  27482  selberg3lem1  27495  selberg4lem1  27498  pntrsumo1  27503  selbergr  27506  pntpbnd1  27524  pntlemk  27544  mulsunif2lem  28108  divsasswd  28142  absmuls  28182  eucliddivs  28301  zscut  28331  expsp1  28352  expadds  28358  pw2divsrecd  28370  pw2cut2  28382  tgbtwnconn1lem3  28552  mideulem2  28712  axlowdimlem16  28935  axcontlem8  28949  vtxval  28978  iedgval  28979  edgval  29027  vtxdgop  29449  finsumvtxdg2size  29529  lp1cycl  30132  ex-ind-dvds  30441  vsfval  30613  lnocoi  30737  nmblolbii  30779  ipasslem5  30815  hvsubid  31006  sshjval3  31334  pjhthlem1  31371  adjval  31870  unopf1o  31896  kbpj  31936  lnopmi  31980  nmcoplbi  32008  cnlnadjlem2  32048  adjadd  32073  branmfn  32085  pjtoi  32159  fconst7v  32603  ofoprabco  32646  supppreima  32672  sgnval2  32718  hashxpe  32789  ccatws1f1o  32932  splfv3  32939  xrsmulgzz  32990  mndractfo  33010  mndlactf1o  33011  mndractf1o  33012  gsumfs2d  33035  psgnfzto1stlem  33069  cycpmco2lem5  33099  cycpmco2lem6  33100  cyc3co2  33109  tocyccntz  33113  cyc3genpmlem  33120  cyc3conja  33126  archiabllem1a  33160  gsumvsca1  33195  gsumvsca2  33196  elrgspnlem2  33210  elrgspnsubrunlem1  33214  rloccring  33237  imaslmod  33318  elrspunidl  33393  mxidlirredi  33436  opprabs  33447  qsdrngi  33460  1arithidomlem1  33500  1arithidomlem2  33501  zringfrac  33519  ressply1evls1  33528  psrbasfsupp  33572  mplvrpmga  33575  ply1degltdimlem  33635  fedgmullem1  33642  fldextrspunlsplem  33686  extdgfialglem2  33706  algextdeglem4  33733  constrconj  33758  constrdircl  33778  constrremulcl  33780  constrimcl  33783  constrresqrtcl  33790  cos9thpiminplylem2  33796  submat1n  33818  submatres  33819  madjusmdetlem3  33842  xrge0iifhom  33950  qqhval2lem  33994  qqhrhm  34002  qqhucn  34005  esumsnf  34077  measvunilem0  34226  carsgclctunlem1  34330  ballotlemfp1  34505  ballotlemsf1o  34527  signstfveq0  34590  breprexplemc  34645  breprexp  34646  breprexpnat  34647  circlemeth  34653  logdivsqrle  34663  hgt750lema  34670  revwlk  35169  cvmlift3lem2  35364  cvmlift3lem4  35366  cvmlift3lem5  35367  cvmlift3lem6  35368  cvmlift3lem9  35371  elmrsubrn  35564  bccolsum  35783  bj-bary1lem  37354  finixpnum  37655  poimirlem4  37674  poimirlem16  37686  poimirlem19  37689  poimirlem25  37695  mblfinlem3  37709  dvtan  37720  itg2addnc  37724  itgaddnclem2  37729  ftc1anclem6  37748  areacirclem5  37762  areacirc  37763  upixp  37779  prdsbnd2  37845  ismrer1  37888  rngoneglmul  37993  rngoisocnv  38031  ecun  38427  islshpsm  39089  lshpnel2N  39094  lfl0f  39178  ldualvsdi1  39252  ldualgrplem  39254  cmtcomlemN  39357  cvlsupr8  39458  pmodl42N  39960  pmapjat1  39962  llnmod2i2  39972  dalawlem2  39981  pmapj2N  40038  idltrn  40259  cdlemc6  40305  cdleme20d  40421  cdleme22e  40453  cdleme22eALTN  40454  cdleme35b  40559  cdleme48fvg  40609  cdlemg4d  40722  cdlemg8a  40736  cdlemg42  40838  cdlemg47a  40843  tendodi1  40893  tendodi2  40894  cdlemk4  40943  cdlemk21N  40982  cdlemk22  41002  cdlemky  41035  cdlemk53b  41065  cdlemk53  41066  cdlemkyyN  41071  erngdvlem3-rN  41107  tendocnv  41130  dia1dim2  41171  dicvaddcl  41299  dihglblem3N  41404  dihmeetlem4preN  41415  dihmeet2  41455  lcfl7lem  41608  baerlem3lem1  41816  baerlem5alem1  41817  mapdh6bN  41846  mapdh6cN  41847  mapdh6dN  41848  hdmap1l6b  41920  hdmap1l6c  41921  hdmap1l6d  41922  hdmap14lem13  41989  ofun  42339  grpcominv1  42611  evlselv  42690  flt4lem7  42762  3cubeslem2  42788  3cubeslem3r  42790  3cubeslem4  42792  pellexlem2  42933  rmxyneg  43023  oddcomabszz  43047  acongeq  43086  hausgraph  43308  onsupnmax  43331  tfsconcatrev  43451  naddass1  43496  fsovrfovd  44112  inductionexd  44258  expgrowth  44438  binomcxplemwb  44451  binomcxplemnn0  44452  binomcxplemnotnn0  44459  sumsnd  45133  restuni4  45228  fmuldfeqlem1  45692  cncfmptss  45697  climexp  45715  dvresntr  46026  stoweidlem17  46125  wallispi  46178  dirkertrigeq  46209  dirkercncflem2  46212  fourierdlem30  46245  fourierdlem41  46256  fourierdlem81  46295  fourierdlem103  46317  sge0xp  46537  sge0isummpt2  46540  isomennd  46639  vonioolem1  46788  sigarperm  46968  fcores  47177  imasetpreimafvbijlemfo  47515  fundcmpsurbijinjpreimafv  47517  fundcmpsurinjimaid  47521  prprspr2  47628  opoeALTV  47793  uhgrimisgrgric  48041  isubgr3stgrlem2  48077  cznrng  48371  rngchomrnghmresALTV  48389  fdmdifeqresdif  48452  lincsum  48540  lincscm  48541  lmod1lem4  48601  blennngt2o2  48703  blennn0e2  48705  tposideq  48998  topdlat  49114  sectpropdlem  49147  invpropdlem  49149  isopropdlem  49151  imaidfu  49221  imasubc  49262  natoppf  49340  swapfid  49390  swapfcoa  49392  fucoppcid  49519  fucoppcco  49520  oppfdiag1  49525  diag1f1olem  49644  oppgoppchom  49701  oppgoppcco  49702  oppgoppcid  49703  2arwcat  49711  reccot  49869  rectan  49870  cotsqcscsq  49873  amgmlemALT  49914