Theorem 3eqtr3i 2457

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

Syntax hints:   = wceq 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-cleq 2412

This theorem is referenced by:  un12  3621  in12  3670  indif1  3714  difundi  3722  difundir  3723  difindi  3724  difindir  3725  dif32  3733  csbvarg  3817  undif1  3867  resmpt3  5166  xp0  5266  fresaunres2  5763  fvsnun1  6105  caov12  6502  caov13  6504  caov411  6506  caovdir  6508  orduniss2  6665  fparlem3  6900  fparlem4  6901  hartogslem1  8048  kmlem3  8571  cdaassen  8601  xpcdaen  8602  halfnq  9390  reclem3pr  9463  addcmpblnr  9482  ltsrpr  9490  pn0sr  9514  sqgt0sr  9519  map2psrpr  9523  negsubdii  9949  halfpm6th  10823  i4  12363  nn0opthlem1  12440  fac4  12453  imi  13188  bpoly3  14078  ef01bndlem  14205  bitsres  14410  gcdaddmlem  14455  modsubi  15004  gcdmodi  15006  numexpp1  15010  karatsuba  15016  oppgcntr  16968  frgpuplem  17363  ressmpladd  18622  ressmplmul  18623  ressmplvsca  18624  ltbwe  18637  ressply1add  18764  ressply1mul  18765  ressply1vsca  18766  sn0cld  20043  qtopres  20650  itg1addlem5  22565  cospi  23331  sincos4thpi  23372  sincos3rdpi  23375  dvlog  23500  dvlog2  23502  dvsqrt  23586  dvcnsqrt  23588  ang180lem3  23644  1cubrlem  23671  mcubic  23677  quart1lem  23685  atantayl2  23768  log2cnv  23774  log2ublem2  23777  log2ub  23779  gam1  23894  chtub  24042  bclbnd  24110  bposlem8  24121  lgsdir2lem1  24153  lgsdir2lem5  24157  ipidsq  26235  ip1ilem  26353  ipdirilem  26356  ipasslem10  26366  siilem1  26378  hvmul2negi  26577  hvadd12i  26586  hvnegdii  26591  normlem1  26639  normlem9  26647  normsubi  26670  normpar2i  26685  polid2i  26686  chjassi  27015  chj12i  27051  pjoml2i  27114  hoadd12i  27306  lnophmlem2  27546  nmopcoadj2i  27631  indifundif  28029  aciunf1  28146  partfun  28159  ffsrn  28198  archirngz  28385  sqsscirc1  28594  sigaclfu2  28823  eulerpartlemd  29066  coinflippvt  29184  ballotth  29237  quad3  30131  onint1  30935  bj-csbsn  31297  cnambfre  31737  rabren3dioph  35411  arearect  35847  areaquad  35848  lhe4.4ex1a  36363  expgrowthi  36367  expgrowth  36369  binomcxplemnotnn0  36390  dvcosre  37401  stoweidlem34  37512  fouriersw  37711