Theorem 3eqtr4ri 2853

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

Syntax hints:   = wceq 1531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-9 2118  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-cleq 2812

This theorem is referenced by:  cbvreucsf  3925  dfin3  4241  dfsymdif3  4267  dfif6  4468  dfsn2ALT  4579  qdass  4681  tpidm12  4683  unipr  4843  iinvdif  4993  unidif0  5251  csbcnv  5747  dfdm4  5757  dmun  5772  domepOLD  5787  resres  5859  inres  5864  resdifcom  5865  resiun1  5866  imainrect  6031  cnvcnv  6042  coundi  6093  coundir  6094  funopg  6382  csbov  7191  elrnmpores  7280  offres  7676  1st2val  7709  2nd2val  7710  mpomptsx  7754  oeoalem  8214  omopthlem1  8274  snec  8352  tcsni  9177  infmap2  9632  ackbij2lem3  9655  itunisuc  9833  axmulass  10571  divmul13i  11393  dfnn3  11644  halfpm6th  11850  numsucc  12130  decbin2  12231  uzrdgxfr  13327  hashxplem  13786  prprrab  13823  ids1  13943  s3s4  14287  s2s5  14288  s5s2  14289  fsumadd  15088  fsum2d  15118  fprodmul  15306  bpoly3  15404  bezout  15883  ressbas  16546  oppchomf  16982  smndex1iidm  18058  symgbas  18491  oppr1  19376  opsrtoslem1  20256  m2detleiblem2  21229  txswaphmeolem  22404  cnfldnm  23379  cnrbas  23738  cnnm  23756  volres  24121  voliunlem1  24143  uniioombllem4  24179  itg11  24284  dfrelog  25141  log2ublem3  25518  bposlem8  25859  uhgrspan1  27077  ip2i  28597  bcseqi  28889  hilnormi  28932  cmcmlem  29360  fh3i  29392  fh4i  29393  pjadjii  29443  cnvoprabOLD  30448  resf1o  30458  dp3mul10  30567  dpmul4  30583  threehalves  30584  ressplusf  30630  cycpmconjs  30791  resvsca  30896  xpinpreima  31142  cnre2csqima  31147  esum2dlem  31344  eulerpartgbij  31623  ballotth  31788  plymulx  31811  hgt750lem2  31916  elrn3  32991  itg2addnclem2  34936  dfcoss3  35654  cossid  35712  dfssr2  35731  rabdif  39097  areaquad  39813  cnvrcl0  39975  stoweidlem13  42288  wallispi2  42348  fourierdlem96  42477  fourierdlem97  42478  fourierdlem98  42479  fourierdlem99  42480  fourierdlem113  42494  fourierswlem  42505  dfafv2  43321  dfnelbr2  43462  fmtnorec2  43695  fmtno5fac  43734  setrec2  44788