Theorem 3eqtr4ri 2768

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

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726

This theorem is referenced by:  cbvreucsf  3891  dfin3  4227  dfsymdif3  4256  rabdif  4271  dfif6  4480  dfsn2ALT  4600  qdass  4708  tpidm12  4710  iinvdif  5033  unidif0  5303  csbcnv  5830  dfdm4  5842  dmun  5857  resres  5949  inres  5954  resdifcom  5955  resiun1  5956  imainrect  6137  cnvcnv  6148  coundi  6203  coundir  6204  funopg  6524  csbov  7401  elrnmpores  7494  offres  7925  1st2val  7959  2nd2val  7960  mpomptsx  8006  oeoalem  8522  omopthlem1  8585  snec  8713  tcsni  9648  infmap2  10125  ackbij2lem3  10148  itunisuc  10327  axmulass  11066  divmul13i  11900  dfnn3  12157  numsucc  12645  decbin2  12746  uzrdgxfr  13888  hashxplem  14354  prprrab  14394  ids1  14519  s3s4  14854  s2s5  14855  s5s2  14856  fsumadd  15661  fsum2d  15692  fprodmul  15881  bpoly3  15979  bezout  16468  oppchomf  17641  dfinito3  17927  dftermo3  17928  smndex1iidm  18824  symgbas  19299  oppr1  20284  opsrtoslem1  22008  m2detleiblem2  22570  txswaphmeolem  23746  cnfldnm  24720  cnrbas  25096  cnnm  25114  volres  25483  voliunlem1  25505  uniioombllem4  25541  itg11  25646  dfrelog  26528  log2ublem3  26912  bposlem8  27256  noinfbnd2  27697  addsasslem1  27973  bdaypw2n0s  28420  uhgrspan1  29325  ip2i  30852  bcseqi  31144  hilnormi  31187  cmcmlem  31615  fh3i  31647  fh4i  31648  pjadjii  31698  resf1o  32758  dp3mul10  32928  dpmul4  32944  threehalves  32945  ressplusf  32994  cycpmconjs  33187  resvsca  33362  cos9thpiminplylem5  33892  xpinpreima  34012  cnre2csqima  34017  esum2dlem  34198  eulerpartgbij  34478  ballotth  34644  plymulx  34654  hgt750lem2  34758  elrn3  35905  itg2addnclem2  37812  dfsucmap3  38576  dfsucmap4  38578  dfcoss3  38616  cossid  38682  dfssr2  38691  dfblockliftfix2  38836  areaquad  43400  cnvrcl0  43808  stoweidlem13  46199  wallispi2  46259  fourierdlem96  46388  fourierdlem97  46389  fourierdlem98  46390  fourierdlem99  46391  fourierdlem113  46405  fourierswlem  46416  dfafv2  47320  dfnelbr2  47461  ceil5half3  47528  fmtnorec2  47731  fmtno5fac  47770  tposrescnv  49066  tposres3  49068  dfswapf2  49448  setrec2  49882