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  3882  dfin3  4218  dfsymdif3  4247  rabdif  4262  dfif6  4470  dfsn2ALT  4590  qdass  4698  tpidm12  4700  iinvdif  5023  unidif0  5295  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  7403  elrnmpores  7496  offres  7927  1st2val  7961  2nd2val  7962  mpomptsx  8008  oeoalem  8523  omopthlem1  8586  snec  8716  tcsni  9651  infmap2  10128  ackbij2lem3  10151  itunisuc  10330  axmulass  11069  divmul13i  11905  dfnn3  12177  numsucc  12673  decbin2  12774  uzrdgxfr  13918  hashxplem  14384  prprrab  14424  ids1  14549  s3s4  14884  s2s5  14885  s5s2  14886  fsumadd  15691  fsum2d  15722  fprodmul  15914  bpoly3  16012  bezout  16501  oppchomf  17675  dfinito3  17961  dftermo3  17962  smndex1iidm  18858  symgbas  19336  oppr1  20319  opsrtoslem1  22042  m2detleiblem2  22602  txswaphmeolem  23778  cnfldnm  24752  cnrbas  25118  cnnm  25136  volres  25504  voliunlem1  25526  uniioombllem4  25562  itg11  25667  dfrelog  26545  log2ublem3  26929  bposlem8  27273  noinfbnd2  27714  addsasslem1  28014  bdaypw2n0bndlem  28474  uhgrspan1  29391  ip2i  30919  bcseqi  31211  hilnormi  31254  cmcmlem  31682  fh3i  31714  fh4i  31715  pjadjii  31765  resf1o  32823  dp3mul10  32977  dpmul4  32993  threehalves  32994  ressplusf  33043  cycpmconjs  33237  resvsca  33412  cos9thpiminplylem5  33951  xpinpreima  34071  cnre2csqima  34076  esum2dlem  34257  eulerpartgbij  34537  ballotth  34703  plymulx  34713  hgt750lem2  34817  elrn3  35965  itg2addnclem2  38004  dfsucmap3  38795  dfsucmap4  38797  dfcoss3  38836  cossid  38902  dfssr2  38911  dfpetparts2  39304  dfpeters2  39306  areaquad  43659  cnvrcl0  44067  stoweidlem13  46456  wallispi2  46516  fourierdlem96  46645  fourierdlem97  46646  fourierdlem98  46647  fourierdlem99  46648  fourierdlem113  46662  fourierswlem  46673  dfafv2  47577  dfnelbr2  47718  ceil5half3  47791  fmtnorec2  48003  fmtno5fac  48042  tposrescnv  49351  tposres3  49353  dfswapf2  49733  setrec2  50167