Theorem 3eqtr4ri 2764

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  cbvreucsf  3909  dfin3  4243  dfsymdif3  4272  rabdif  4287  dfif6  4494  dfsn2ALT  4614  qdass  4720  tpidm12  4722  iinvdif  5047  unidif0  5318  csbcnv  5850  dfdm4  5862  dmun  5877  resres  5966  inres  5971  resdifcom  5972  resiun1  5973  imainrect  6157  cnvcnv  6168  coundi  6223  coundir  6224  funopg  6553  csbov  7435  elrnmpores  7530  offres  7965  1st2val  7999  2nd2val  8000  mpomptsx  8046  oeoalem  8563  omopthlem1  8626  snec  8754  tcsni  9703  infmap2  10177  ackbij2lem3  10200  itunisuc  10379  axmulass  11117  divmul13i  11950  dfnn3  12207  numsucc  12696  decbin2  12797  uzrdgxfr  13939  hashxplem  14405  prprrab  14445  ids1  14569  s3s4  14906  s2s5  14907  s5s2  14908  fsumadd  15713  fsum2d  15744  fprodmul  15933  bpoly3  16031  bezout  16520  oppchomf  17688  dfinito3  17974  dftermo3  17975  smndex1iidm  18835  symgbas  19309  oppr1  20266  opsrtoslem1  21969  m2detleiblem2  22522  txswaphmeolem  23698  cnfldnm  24673  cnrbas  25049  cnnm  25067  volres  25436  voliunlem1  25458  uniioombllem4  25494  itg11  25599  dfrelog  26481  log2ublem3  26865  bposlem8  27209  noinfbnd2  27650  addsasslem1  27917  uhgrspan1  29237  ip2i  30764  bcseqi  31056  hilnormi  31099  cmcmlem  31527  fh3i  31559  fh4i  31560  pjadjii  31610  resf1o  32660  dp3mul10  32825  dpmul4  32841  threehalves  32842  ressplusf  32892  cycpmconjs  33120  resvsca  33311  cos9thpiminplylem5  33783  xpinpreima  33903  cnre2csqima  33908  esum2dlem  34089  eulerpartgbij  34370  ballotth  34536  plymulx  34546  hgt750lem2  34650  elrn3  35756  itg2addnclem2  37673  dfcoss3  38412  cossid  38478  dfssr2  38497  areaquad  43212  cnvrcl0  43621  stoweidlem13  46018  wallispi2  46078  fourierdlem96  46207  fourierdlem97  46208  fourierdlem98  46209  fourierdlem99  46210  fourierdlem113  46224  fourierswlem  46235  dfafv2  47137  dfnelbr2  47278  ceil5half3  47345  fmtnorec2  47548  fmtno5fac  47587  tposrescnv  48871  tposres3  48873  dfswapf2  49254  setrec2  49688