Theorem 3eqtr3i 2478

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

Syntax hints:   = wceq 1381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-ext 2419

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

This theorem is referenced by:  un12  3644  in12  3691  indif1  3724  difundi  3732  difundir  3733  difindi  3734  difindir  3735  dif32  3743  csbvarg  3830  undif1  3885  resmpt3  5310  xp0  5411  fresaunres2  5743  fvsnun1  6087  caov12  6484  caov13  6486  caov411  6488  caovdir  6490  orduniss2  6649  fparlem3  6883  fparlem4  6884  hartogslem1  7965  kmlem3  8530  cdaassen  8560  xpcdaen  8561  halfnq  9352  reclem3pr  9425  addcmpblnr  9444  ltsrpr  9452  pn0sr  9476  sqgt0sr  9481  map2psrpr  9485  negsubdii  9905  halfpm6th  10761  i4  12244  nn0opthlem1  12322  fac4  12335  imi  12964  ef01bndlem  13791  bitsres  13995  gcdaddmlem  14038  modsubi  14430  gcdmodi  14432  numexpp1  14436  karatsuba  14442  oppgcntr  16269  frgpuplem  16659  ressmpladd  17987  ressmplmul  17988  ressmplvsca  17989  ltbwe  18005  ressply1add  18139  ressply1mul  18140  ressply1vsca  18141  sn0cld  19457  qtopres  20065  itg1addlem5  21973  cospi  22730  sincos4thpi  22771  sincos3rdpi  22774  dvlog  22897  dvlog2  22899  dvsqrt  22983  ang180lem3  23008  1cubrlem  23037  mcubic  23043  quart1lem  23051  atantayl2  23134  log2cnv  23140  log2ublem2  23143  log2ub  23145  chtub  23352  bclbnd  23420  bposlem8  23431  lgsdir2lem1  23463  lgsdir2lem5  23467  ipidsq  25488  ip1ilem  25606  ipdirilem  25609  ipasslem10  25619  siilem1  25631  hvmul2negi  25830  hvadd12i  25839  hvnegdii  25844  normlem1  25892  normlem9  25900  normsubi  25923  normpar2i  25938  polid2i  25939  chjassi  26269  chj12i  26305  pjoml2i  26368  hoadd12i  26561  lnophmlem2  26801  nmopcoadj2i  26886  partfun  27381  ffsrn  27417  archirngz  27599  sqsscirc1  27756  sigaclfu2  27987  eulerpartlemd  28171  coinflippvt  28289  ballotth  28342  gam1  28473  quad3  28890  bpoly3  29788  onint1  29882  cnambfre  30031  dvcnsqrt  30069  rabren3dioph  30717  arearect  31152  areaquad  31153  lhe4.4ex1a  31203  expgrowthi  31207  expgrowth  31209  dvcosre  31606  stoweidlem34  31701  fouriersw  31899  bj-csbsn  34183