Theorem 3eqtr4ri 2797

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  cbvreucsf  3895  dfin3  4225  dfsymdif3  4254  rabdif  4269  dfif6  4488  dfsn2ALT  4606  qdass  4716  tpidm12  4718  iinvdif  5045  unidif0OLD  5329  csbcnvOLD  5877  dfdm4  5889  dmun  5904  resres  5999  inres  6004  resdifcom  6005  resiun1  6006  imainrect  6191  cnvcnv  6202  coundi  6267  coundir  6268  funopg  6602  csbov  7496  elrnmpores  7590  offres  8029  1st2val  8063  2nd2val  8064  mpomptsx  8110  oeoalem  8643  omopthlem1  8706  snec  8837  tcsni  9779  dfhf2  9943  setrec2  10014  infmap2  10334  ackbij2lem3  10357  itunisuc  10536  axmulass  11281  divmul13i  12118  dfnn3  12389  numsucc  12899  decbin2  13002  uzrdgxfr  14150  hashxplem  14619  prprrab  14659  ids1  14785  s3s4  15127  s2s5  15128  s5s2  15129  fsumadd  15950  fsum2d  15981  fprodmul  16171  bpoly3  16268  bezout  16760  oppchomf  17944  dfinito3  18230  dftermo3  18231  smndex1iidm  19147  symgbas  19637  oppr1  20631  opsrtoslem1  22419  m2detleiblem2  22998  txswaphmeolem  24178  cnfldnm  25152  cnrbas  25518  cnnm  25536  volres  25904  voliunlem1  25926  uniioombllem4  25962  itg11  26067  plymulidp  26658  dfrelog  26950  log2ublem3  27333  bposlem8  27675  noinfbnd2  28145  addsasslem1  28446  bdaypw2n0bndlem  28906  uhgrspan1  29941  ip2i  31487  bcseqi  31779  hilnormi  31822  cmcmlem  32250  fh3i  32282  fh4i  32283  pjadjii  32333  resf1o  33418  dp3mul10  33560  dpmul4  33576  threehalves  33577  ressplusf  33620  cycpmconjs  33816  resvsca  33997  cos9thpiminplylem5  34529  xpinpreima  34649  cnre2csqima  34654  esum2dlem  34835  eulerpartgbij  35115  ballotth  35281  hgt750lem2  35392  elrn3  36742  itg2addnclem2  38858  dfsucmap3  39661  dfsucmap4  39663  dfcoss3  39702  cossid  39768  dfssr2  39777  dfpetparts2  40170  dfpeters2  40172  areaquad  44479  cnvrcl0  44886  stoweidlem13  47296  wallispi2  47356  fourierdlem96  47485  fourierdlem97  47486  fourierdlem98  47487  fourierdlem99  47488  fourierdlem113  47502  fourierswlem  47513  goldpolyfactor  48200  goldratval  48209  dfafv2  48475  dfnelbr2  48616  ceil5half3  48689  fmtnorec2  48901  fmtno5fac  48940  bru3val  49753  ehl2eudisval0  50169  itscnhlinecirc02plem3  50227  inlinecirc02p  50230  tposrescnv  50323  tposres3  50325  dfswapf2  50714