Theorem 3eqtr4ri 2769

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

Syntax hints:   = wceq 1539

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  cbvreucsf  3939  dfin3  4265  dfsymdif3  4295  dfif6  4530  dfsn2ALT  4647  qdass  4756  tpidm12  4758  uniprOLD  4926  iinvdif  5082  unidif0  5357  csbcnv  5882  dfdm4  5894  dmun  5909  resres  5993  inres  5998  resdifcom  5999  resiun1  6000  imainrect  6179  cnvcnv  6190  coundi  6245  coundir  6246  funopg  6581  csbov  7454  elrnmpores  7548  offres  7972  1st2val  8005  2nd2val  8006  mpomptsx  8052  oeoalem  8598  omopthlem1  8660  snec  8776  tcsni  9740  infmap2  10215  ackbij2lem3  10238  itunisuc  10416  axmulass  11154  divmul13i  11979  dfnn3  12230  halfpm6th  12437  numsucc  12721  decbin2  12822  uzrdgxfr  13936  hashxplem  14397  prprrab  14438  ids1  14551  s3s4  14888  s2s5  14889  s5s2  14890  fsumadd  15690  fsum2d  15721  fprodmul  15908  bpoly3  16006  bezout  16489  ressbasOLD  17184  oppchomf  17670  dfinito3  17959  dftermo3  17960  smndex1iidm  18818  symgbas  19279  oppr1  20241  opsrtoslem1  21835  m2detleiblem2  22350  txswaphmeolem  23528  cnfldnm  24515  cnrbas  24889  cnnm  24908  volres  25277  voliunlem1  25299  uniioombllem4  25335  itg11  25440  dfrelog  26310  log2ublem3  26689  bposlem8  27030  noinfbnd2  27470  addsasslem1  27725  uhgrspan1  28827  ip2i  30348  bcseqi  30640  hilnormi  30683  cmcmlem  31111  fh3i  31143  fh4i  31144  pjadjii  31194  cnvoprabOLD  32212  resf1o  32222  dp3mul10  32331  dpmul4  32347  threehalves  32348  ressplusf  32394  cycpmconjs  32585  resvsca  32714  xpinpreima  33184  cnre2csqima  33189  esum2dlem  33388  eulerpartgbij  33669  ballotth  33834  plymulx  33857  hgt750lem2  33962  elrn3  35036  itg2addnclem2  36843  dfcoss3  37587  cossid  37653  dfssr2  37672  rabdif  41338  areaquad  42267  cnvrcl0  42678  stoweidlem13  45027  wallispi2  45087  fourierdlem96  45216  fourierdlem97  45217  fourierdlem98  45218  fourierdlem99  45219  fourierdlem113  45233  fourierswlem  45244  dfafv2  46138  dfnelbr2  46279  fmtnorec2  46509  fmtno5fac  46548  setrec2  47827