Theorem 3eqtr4ri 2803

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

Syntax hints:   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  cbvreucsf  3905  dfin3  4238  dfsymdif3  4267  rabdif  4282  dfif6  4495  dfsn2ALT  4616  qdass  4724  tpidm12  4726  iinvdif  5050  unidif0OLD  5332  csbcnvOLD  5874  dfdm4  5886  dmun  5901  resres  5992  inres  5997  resdifcom  5998  resiun1  5999  imainrect  6180  cnvcnv  6191  coundi  6249  coundir  6250  funopg  6571  csbov  7456  elrnmpores  7549  offres  7979  1st2val  8013  2nd2val  8014  mpomptsx  8060  oeoalem  8581  omopthlem1  8644  snec  8775  tcsni  9709  infmap2  10199  ackbij2lem3  10222  itunisuc  10402  axmulass  11141  divmul13i  11975  dfnn3  12246  numsucc  12755  decbin2  12858  uzrdgxfr  14002  hashxplem  14469  prprrab  14509  ids1  14634  s3s4  14969  s2s5  14970  s5s2  14971  fsumadd  15790  fsum2d  15821  fprodmul  16013  bpoly3  16111  bezout  16600  oppchomf  17775  dfinito3  18061  dftermo3  18062  smndex1iidm  18959  symgbas  19441  oppr1  20431  opsrtoslem1  22174  m2detleiblem2  22753  txswaphmeolem  23929  cnfldnm  24903  cnrbas  25269  cnnm  25287  volres  25655  voliunlem1  25677  uniioombllem4  25713  itg11  25818  plymulidp  26411  dfrelog  26695  log2ublem3  27078  bposlem8  27420  noinfbnd2  27860  addsasslem1  28161  bdaypw2n0bndlem  28621  uhgrspan1  29593  ip2i  31120  bcseqi  31412  hilnormi  31455  cmcmlem  31883  fh3i  31915  fh4i  31916  pjadjii  31966  resf1o  33015  dp3mul10  33157  dpmul4  33173  threehalves  33174  ressplusf  33223  cycpmconjs  33416  resvsca  33594  cos9thpiminplylem5  34120  xpinpreima  34240  cnre2csqima  34245  esum2dlem  34426  eulerpartgbij  34706  ballotth  34872  hgt750lem2  34983  elrn3  36152  itg2addnclem2  38210  dfsucmap3  39001  dfsucmap4  39003  dfcoss3  39042  cossid  39108  dfssr2  39117  dfpetparts2  39510  dfpeters2  39512  areaquad  43834  cnvrcl0  44242  stoweidlem13  46618  wallispi2  46678  fourierdlem96  46807  fourierdlem97  46808  fourierdlem98  46809  fourierdlem99  46810  fourierdlem113  46824  fourierswlem  46835  dfafv2  47757  dfnelbr2  47898  ceil5half3  47971  fmtnorec2  48183  fmtno5fac  48222  tposrescnv  49541  tposres3  49543  dfswapf2  49923  setrec2  50357