Theorem 3eqtr3i 2471

Description: An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr3i.1	|- A = B
3eqtr3i.2	|- A = C
3eqtr3i.3	|- B = D

Assertion

Ref	Expression
3eqtr3i	|- C = D

Proof of Theorem 3eqtr3i

Step	Hyp	Ref	Expression
1		3eqtr3i.1	. . 3 |- A = B
2		3eqtr3i.2	. . 3 |- A = C
3	1, 2	eqtr3i 2465	. 2 |- B = C
4		3eqtr3i.3	. 2 |- B = D
5	3, 4	eqtr3i 2465	1 |- C = D

Syntax hints:   = wceq 1369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436

This theorem is referenced by:  un12  3526  in12  3573  indif1  3606  difundi  3614  difundir  3615  difindi  3616  difindir  3617  dif32  3625  csbvarg  3712  undif1  3766  resmpt3  5169  xp0  5268  fresaunres2  5595  fvsnun1  5925  caov12  6303  caov13  6305  caov411  6307  caovdir  6309  orduniss2  6456  fparlem3  6686  fparlem4  6687  hartogslem1  7768  kmlem3  8333  cdaassen  8363  xpcdaen  8364  halfnq  9157  reclem3pr  9230  addcmpblnr  9251  ltsrpr  9256  pn0sr  9280  sqgt0sr  9285  map2psrpr  9289  negsubdii  9705  halfpm6th  10558  i4  11980  nn0opthlem1  12058  fac4  12071  imi  12658  ef01bndlem  13480  bitsres  13681  gcdaddmlem  13724  modsubi  14113  gcdmodi  14115  numexpp1  14119  karatsuba  14125  oppgcntr  15892  frgpuplem  16281  ressmpladd  17548  ressmplmul  17549  ressmplvsca  17550  ltbwe  17566  ressply1add  17696  ressply1mul  17697  ressply1vsca  17698  sn0cld  18706  qtopres  19283  itg1addlem5  21190  cospi  21946  sincos4thpi  21987  sincos3rdpi  21990  dvlog  22108  dvlog2  22110  dvsqr  22194  ang180lem3  22219  1cubrlem  22248  mcubic  22254  quart1lem  22262  atantayl2  22345  log2cnv  22351  log2ublem2  22354  log2ub  22356  chtub  22563  bclbnd  22631  bposlem8  22642  lgsdir2lem1  22674  lgsdir2lem5  22678  ipidsq  24120  ip1ilem  24238  ipdirilem  24241  ipasslem10  24251  siilem1  24263  hvmul2negi  24462  hvadd12i  24471  hvnegdii  24476  normlem1  24524  normlem9  24532  normsubi  24555  normpar2i  24570  polid2i  24571  chjassi  24901  chj12i  24937  pjoml2i  25000  hoadd12i  25193  lnophmlem2  25433  nmopcoadj2i  25518  partfun  26005  archirngz  26218  sqsscirc1  26350  sigaclfu2  26576  eulerpartlemd  26761  coinflippvt  26879  ballotth  26932  gam1  27063  bpoly3  28213  onint1  28307  cnambfre  28452  dvcnsqr  28490  rabren3dioph  29166  arearect  29603  areaquad  29604  lhe4.4ex1a  29615  expgrowthi  29619  expgrowth  29621  dvcosre  29800  stoweidlem34  29841  bj-csbsn  32418