Theorem 3eqtr4ri 2773

Description: An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr4i.1	⊢ 𝐴 = 𝐵
3eqtr4i.2	⊢ 𝐶 = 𝐴
3eqtr4i.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3eqtr4ri	⊢ 𝐷 = 𝐶

Proof of Theorem 3eqtr4ri

Step	Hyp	Ref	Expression
1		3eqtr4i.3	. . 3 ⊢ 𝐷 = 𝐵
2		3eqtr4i.1	. . 3 ⊢ 𝐴 = 𝐵
3	1, 2	eqtr4i 2765	. 2 ⊢ 𝐷 = 𝐴
4		3eqtr4i.2	. 2 ⊢ 𝐶 = 𝐴
5	3, 4	eqtr4i 2765	1 ⊢ 𝐷 = 𝐶

Syntax hints:   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  cbvreucsf  3875  dfin3  4205  dfsymdif3  4234  rabdif  4249  dfif6  4457  dfsn2ALT  4577  qdass  4685  tpidm12  4687  iinvdif  5009  unidif0OLD  5289  csbcnv  5825  dfdm4  5837  dmun  5852  resres  5944  inres  5949  resdifcom  5950  resiun1  5951  imainrect  6132  cnvcnv  6143  coundi  6198  coundir  6199  funopg  6519  csbov  7401  elrnmpores  7494  offres  7925  1st2val  7959  2nd2val  7960  mpomptsx  8006  oeoalem  8522  omopthlem1  8585  snec  8715  tcsni  9653  infmap2  10130  ackbij2lem3  10153  itunisuc  10332  axmulass  11071  divmul13i  11907  dfnn3  12179  numsucc  12675  decbin2  12776  uzrdgxfr  13920  hashxplem  14386  prprrab  14426  ids1  14551  s3s4  14886  s2s5  14887  s5s2  14888  fsumadd  15693  fsum2d  15724  fprodmul  15916  bpoly3  16014  bezout  16503  oppchomf  17677  dfinito3  17963  dftermo3  17964  smndex1iidm  18860  symgbas  19338  oppr1  20321  opsrtoslem1  22031  m2detleiblem2  22611  txswaphmeolem  23787  cnfldnm  24761  cnrbas  25127  cnnm  25145  volres  25513  voliunlem1  25535  uniioombllem4  25571  itg11  25676  dfrelog  26547  log2ublem3  26930  bposlem8  27272  noinfbnd2  27713  addsasslem1  28013  bdaypw2n0bndlem  28473  uhgrspan1  29390  ip2i  30917  bcseqi  31209  hilnormi  31252  cmcmlem  31680  fh3i  31712  fh4i  31713  pjadjii  31763  resf1o  32822  dp3mul10  32976  dpmul4  32992  threehalves  32993  ressplusf  33042  cycpmconjs  33237  resvsca  33415  cos9thpiminplylem5  33970  xpinpreima  34090  cnre2csqima  34095  esum2dlem  34276  eulerpartgbij  34556  ballotth  34722  plymulx  34732  hgt750lem2  34836  elrn3  35990  itg2addnclem2  38039  dfsucmap3  38830  dfsucmap4  38832  dfcoss3  38871  cossid  38937  dfssr2  38946  dfpetparts2  39339  dfpeters2  39341  areaquad  43661  cnvrcl0  44069  stoweidlem13  46456  wallispi2  46516  fourierdlem96  46645  fourierdlem97  46646  fourierdlem98  46647  fourierdlem99  46648  fourierdlem113  46662  fourierswlem  46673  dfafv2  47595  dfnelbr2  47736  ceil5half3  47809  fmtnorec2  48021  fmtno5fac  48060  tposrescnv  49369  tposres3  49371  dfswapf2  49751  setrec2  50185