Theorem 3eqtr4ri 2771

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

Syntax hints:   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  cbvreucsf  3895  dfin3  4231  dfsymdif3  4260  rabdif  4275  dfif6  4484  dfsn2ALT  4604  qdass  4712  tpidm12  4714  iinvdif  5037  unidif0  5307  csbcnv  5840  dfdm4  5852  dmun  5867  resres  5959  inres  5964  resdifcom  5965  resiun1  5966  imainrect  6147  cnvcnv  6158  coundi  6213  coundir  6214  funopg  6534  csbov  7413  elrnmpores  7506  offres  7937  1st2val  7971  2nd2val  7972  mpomptsx  8018  oeoalem  8534  omopthlem1  8597  snec  8727  tcsni  9662  infmap2  10139  ackbij2lem3  10162  itunisuc  10341  axmulass  11080  divmul13i  11914  dfnn3  12171  numsucc  12659  decbin2  12760  uzrdgxfr  13902  hashxplem  14368  prprrab  14408  ids1  14533  s3s4  14868  s2s5  14869  s5s2  14870  fsumadd  15675  fsum2d  15706  fprodmul  15895  bpoly3  15993  bezout  16482  oppchomf  17655  dfinito3  17941  dftermo3  17942  smndex1iidm  18838  symgbas  19313  oppr1  20298  opsrtoslem1  22022  m2detleiblem2  22584  txswaphmeolem  23760  cnfldnm  24734  cnrbas  25110  cnnm  25128  volres  25497  voliunlem1  25519  uniioombllem4  25555  itg11  25660  dfrelog  26542  log2ublem3  26926  bposlem8  27270  noinfbnd2  27711  addsasslem1  28011  bdaypw2n0bndlem  28471  uhgrspan1  29388  ip2i  30916  bcseqi  31208  hilnormi  31251  cmcmlem  31679  fh3i  31711  fh4i  31712  pjadjii  31762  resf1o  32820  dp3mul10  32990  dpmul4  33006  threehalves  33007  ressplusf  33056  cycpmconjs  33250  resvsca  33425  cos9thpiminplylem5  33964  xpinpreima  34084  cnre2csqima  34089  esum2dlem  34270  eulerpartgbij  34550  ballotth  34716  plymulx  34726  hgt750lem2  34830  elrn3  35978  itg2addnclem2  37923  dfsucmap3  38714  dfsucmap4  38716  dfcoss3  38755  cossid  38821  dfssr2  38830  dfpetparts2  39223  dfpeters2  39225  areaquad  43573  cnvrcl0  43981  stoweidlem13  46371  wallispi2  46431  fourierdlem96  46560  fourierdlem97  46561  fourierdlem98  46562  fourierdlem99  46563  fourierdlem113  46577  fourierswlem  46588  dfafv2  47492  dfnelbr2  47633  ceil5half3  47700  fmtnorec2  47903  fmtno5fac  47942  tposrescnv  49238  tposres3  49240  dfswapf2  49620  setrec2  50054