Theorem 3eqtr3i 2504

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 2498	. 2 |- B = C
4		3eqtr3i.3	. 2 |- B = D
5	3, 4	eqtr3i 2498	1 |- C = D

Syntax hints:   = wceq 1379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-cleq 2459

This theorem is referenced by:  un12  3662  in12  3709  indif1  3742  difundi  3750  difundir  3751  difindi  3752  difindir  3753  dif32  3761  csbvarg  3848  undif1  3902  resmpt3  5323  xp0  5424  fresaunres2  5756  fvsnun1  6095  caov12  6486  caov13  6488  caov411  6490  caovdir  6492  orduniss2  6647  fparlem3  6885  fparlem4  6886  hartogslem1  7966  kmlem3  8531  cdaassen  8561  xpcdaen  8562  halfnq  9353  reclem3pr  9426  addcmpblnr  9445  ltsrpr  9453  pn0sr  9477  sqgt0sr  9482  map2psrpr  9486  negsubdii  9903  halfpm6th  10759  i4  12237  nn0opthlem1  12315  fac4  12328  imi  12952  ef01bndlem  13779  bitsres  13981  gcdaddmlem  14024  modsubi  14416  gcdmodi  14418  numexpp1  14422  karatsuba  14428  oppgcntr  16202  frgpuplem  16593  ressmpladd  17906  ressmplmul  17907  ressmplvsca  17908  ltbwe  17924  ressply1add  18058  ressply1mul  18059  ressply1vsca  18060  sn0cld  19373  qtopres  19950  itg1addlem5  21858  cospi  22614  sincos4thpi  22655  sincos3rdpi  22658  dvlog  22776  dvlog2  22778  dvsqrt  22862  ang180lem3  22887  1cubrlem  22916  mcubic  22922  quart1lem  22930  atantayl2  23013  log2cnv  23019  log2ublem2  23022  log2ub  23024  chtub  23231  bclbnd  23299  bposlem8  23310  lgsdir2lem1  23342  lgsdir2lem5  23346  ipidsq  25315  ip1ilem  25433  ipdirilem  25436  ipasslem10  25446  siilem1  25458  hvmul2negi  25657  hvadd12i  25666  hvnegdii  25671  normlem1  25719  normlem9  25727  normsubi  25750  normpar2i  25765  polid2i  25766  chjassi  26096  chj12i  26132  pjoml2i  26195  hoadd12i  26388  lnophmlem2  26628  nmopcoadj2i  26713  partfun  27204  archirngz  27411  sqsscirc1  27542  sigaclfu2  27777  eulerpartlemd  27961  coinflippvt  28079  ballotth  28132  gam1  28263  bpoly3  29413  onint1  29507  cnambfre  29656  dvcnsqrt  29694  rabren3dioph  30369  arearect  30804  areaquad  30805  lhe4.4ex1a  30850  expgrowthi  30854  expgrowth  30856  dvcosre  31255  stoweidlem34  31350  bj-csbsn  33561