Theorem 3eqtr4ri 2794

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 2786	. 2 ⊢ 𝐷 = 𝐴
4		3eqtr4i.2	. 2 ⊢ 𝐶 = 𝐴
5	3, 4	eqtr4i 2786	1 ⊢ 𝐷 = 𝐶

This proof depends on syntax axioms:   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  cbvreucsf  3891  dfin3  4221  dfsymdif3  4250  rabdif  4265  dfif6  4484  dfsn2ALT  4602  qdass  4710  tpidm12  4712  iinvdif  5039  unidif0OLD  5322  csbcnvOLD  5866  dfdm4  5878  dmun  5893  resres  5984  inres  5989  resdifcom  5990  resiun1  5991  imainrect  6175  cnvcnv  6186  coundi  6251  coundir  6252  funopg  6579  csbov  7469  elrnmpores  7562  offres  7999  1st2val  8033  2nd2val  8034  mpomptsx  8080  oeoalem  8613  omopthlem1  8676  snec  8807  tcsni  9749  dfhf2  9913  setrec2  9984  infmap2  10302  ackbij2lem3  10325  itunisuc  10504  axmulass  11249  divmul13i  12085  dfnn3  12356  numsucc  12866  decbin2  12969  uzrdgxfr  14117  hashxplem  14585  prprrab  14625  ids1  14751  s3s4  15093  s2s5  15094  s5s2  15095  fsumadd  15915  fsum2d  15946  fprodmul  16136  bpoly3  16233  bezout  16725  oppchomf  17903  dfinito3  18189  dftermo3  18190  smndex1iidm  19106  symgbas  19595  oppr1  20589  opsrtoslem1  22373  m2detleiblem2  22952  txswaphmeolem  24132  cnfldnm  25106  cnrbas  25472  cnnm  25490  volres  25858  voliunlem1  25880  uniioombllem4  25916  itg11  26021  plymulidp  26612  dfrelog  26902  log2ublem3  27285  bposlem8  27627  noinfbnd2  28097  addsasslem1  28398  bdaypw2n0bndlem  28858  uhgrspan1  29893  ip2i  31439  bcseqi  31731  hilnormi  31774  cmcmlem  32202  fh3i  32234  fh4i  32235  pjadjii  32285  resf1o  33372  dp3mul10  33514  dpmul4  33530  threehalves  33531  ressplusf  33574  cycpmconjs  33767  resvsca  33943  cos9thpiminplylem5  34468  xpinpreima  34588  cnre2csqima  34593  esum2dlem  34774  eulerpartgbij  35054  ballotth  35220  hgt750lem2  35331  elrn3  36651  itg2addnclem2  38727  dfsucmap3  39532  dfsucmap4  39534  dfcoss3  39573  cossid  39639  dfssr2  39648  dfpetparts2  40041  dfpeters2  40043  areaquad  44355  cnvrcl0  44762  stoweidlem13  47159  wallispi2  47219  fourierdlem96  47348  fourierdlem97  47349  fourierdlem98  47350  fourierdlem99  47351  fourierdlem113  47365  fourierswlem  47376  goldpolyfactor  48063  goldratval  48072  dfafv2  48338  dfnelbr2  48479  ceil5half3  48552  fmtnorec2  48764  fmtno5fac  48803  itscnhlinecirc02plem3  50032  tposrescnv  50128  tposres3  50130  dfswapf2  50519