Theorem 3eqtr2i 2490

Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)

Hypotheses

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

Assertion

Ref	Expression
3eqtr2i	|- A = D

Proof of Theorem 3eqtr2i

Step	Hyp	Ref	Expression
1		3eqtr2i.1	. . 3 |- A = B
2		3eqtr2i.2	. . 3 |- C = B
3	1, 2	eqtr4i 2487	. 2 |- A = C
4		3eqtr2i.3	. 2 |- C = D
5	3, 4	eqtri 2484	1 |- A = D

Syntax hints:   = wceq 1455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-cleq 2455

This theorem is referenced by:  indif  3697  dfrab3  3730  iunid  4347  cnvcnv  5307  cocnvcnv2  5366  fmptap  6111  fpar  6927  fodomr  7749  jech9.3  8311  cda1dif  8632  alephadd  9028  distrnq  9412  ltanq  9422  ltrnq  9430  negdiiOLD  9985  halfpm6th  10863  numma  11111  numaddc  11115  6p5lem  11129  binom2i  12416  faclbnd4lem1  12510  0.999...  13986  6gcd4e2  14551  dfphi2  14771  mod2xnegi  15092  karatsuba  15105  1259lem1  15151  oppgtopn  17053  mgptopn  17781  ply1plusg  18867  ply1vsca  18868  ply1mulr  18869  restcld  20237  cmpsublem  20463  kgentopon  20602  txswaphmeolem  20868  dfii5  21966  itg1climres  22721  ang180lem1  23787  1cubrlem  23816  quart1lem  23830  efiatan  23887  log2cnv  23919  1sgm2ppw  24177  ppiub  24181  bposlem8  24268  bposlem9  24269  ax5seglem7  25014  usgraexmplcvtx  25182  usgraexmplcedg  25183  ipidsq  26398  ipdirilem  26519  norm3difi  26849  polid2i  26859  pjclem3  27899  cvmdi  28026  indifundif  28201  eulerpartlemt  29253  eulerpart  29264  ballotlem1  29368  ballotlemfval0  29377  ballotth  29419  ballotthOLD  29457  subfaclim  29960  kur14lem6  29983  quad3  30351  iexpire  30420  pigt3  31983  volsupnfl  32030  areaquad  36146  wallispilem4  37968  dirkertrigeqlem3  38000  dirkercncflem1  38003  fourierswlem  38132  fouriersw  38133  tgoldbachlt  38947  3exp4mod41  38954  41prothprm  38957  2pthd  39889  3pthd  39915  zlmodzxz0  40410  linevalexample  40461