Theorem 3eqtr3i 2480

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

Syntax hints:   = wceq 1443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-cleq 2443

This theorem is referenced by:  un12  3591  in12  3642  indif1  3686  difundi  3694  difundir  3695  difindi  3696  difindir  3697  dif32  3705  csbvarg  3791  undif1  3841  resmpt3  5154  xp0  5254  fresaunres2  5753  fvsnun1  6097  caov12  6494  caov13  6496  caov411  6498  caovdir  6500  orduniss2  6657  fparlem3  6895  fparlem4  6896  hartogslem1  8054  kmlem3  8579  cdaassen  8609  xpcdaen  8610  halfnq  9398  reclem3pr  9471  addcmpblnr  9490  ltsrpr  9498  pn0sr  9522  sqgt0sr  9527  map2psrpr  9531  negsubdii  9957  halfpm6th  10831  i4  12374  nn0opthlem1  12451  fac4  12464  imi  13213  bpoly3  14104  ef01bndlem  14231  bitsres  14440  gcdaddmlem  14485  modsubi  15037  gcdmodi  15039  numexpp1  15043  karatsuba  15049  oppgcntr  17009  frgpuplem  17415  ressmpladd  18674  ressmplmul  18675  ressmplvsca  18676  ltbwe  18689  ressply1add  18816  ressply1mul  18817  ressply1vsca  18818  sn0cld  20099  qtopres  20706  itg1addlem5  22651  cospi  23420  sincos4thpi  23461  sincos3rdpi  23464  dvlog  23589  dvlog2  23591  dvsqrt  23675  dvcnsqrt  23677  ang180lem3  23733  1cubrlem  23760  mcubic  23766  quart1lem  23774  atantayl2  23857  log2cnv  23863  log2ublem2  23866  log2ub  23868  gam1  23983  chtub  24133  bclbnd  24201  bposlem8  24212  lgsdir2lem1  24244  lgsdir2lem5  24248  ipidsq  26342  ip1ilem  26460  ipdirilem  26463  ipasslem10  26473  siilem1  26485  hvmul2negi  26694  hvadd12i  26703  hvnegdii  26708  normlem1  26756  normlem9  26764  normsubi  26787  normpar2i  26802  polid2i  26803  chjassi  27132  chj12i  27168  pjoml2i  27231  hoadd12i  27423  lnophmlem2  27663  nmopcoadj2i  27748  indifundif  28145  aciunf1  28258  partfun  28271  ffsrn  28307  archirngz  28499  sqsscirc1  28707  sigaclfu2  28936  eulerpartlemd  29192  coinflippvt  29310  ballotth  29363  ballotthOLD  29401  quad3  30295  onint1  31102  bj-csbsn  31499  cnambfre  31982  rabren3dioph  35652  arearect  36094  areaquad  36095  resnonrel  36192  cononrel1  36194  cononrel2  36195  lhe4.4ex1a  36672  expgrowthi  36676  expgrowth  36678  binomcxplemnotnn0  36699  dvcosre  37775  stoweidlem34  37889  fouriersw  38089