Theorem 3eqtr2i 2464

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 2461	. 2 |- A = C
4		3eqtr2i.3	. 2 |- C = D
5	3, 4	eqtri 2458	1 |- A = 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 2407

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

This theorem is referenced by:  indif  3721  dfrab3  3754  iunid  4357  cnvcnv  5308  cocnvcnv2  5367  fmptap  6102  fpar  6911  fodomr  7729  jech9.3  8284  cda1dif  8604  alephadd  9000  distrnq  9385  ltanq  9395  ltrnq  9403  negdiiOLD  9958  halfpm6th  10834  numma  11082  numaddc  11086  6p5lem  11100  binom2i  12381  faclbnd4lem1  12475  0.999...  13915  6gcd4e2  14476  dfphi2  14691  mod2xnegi  15006  karatsuba  15019  1259lem1  15065  oppgtopn  16955  mgptopn  17667  ply1plusg  18753  ply1vsca  18754  ply1mulr  18755  restcld  20119  cmpsublem  20345  kgentopon  20484  txswaphmeolem  20750  dfii5  21813  itg1climres  22549  ang180lem1  23603  1cubrlem  23632  quart1lem  23646  efiatan  23703  log2cnv  23735  1sgm2ppw  23991  ppiub  23995  bposlem8  24082  bposlem9  24083  ax5seglem7  24811  usgraexmplcvtx  24978  usgraexmplcedg  24979  ipidsq  26194  ipdirilem  26315  norm3difi  26635  polid2i  26645  pjclem3  27685  cvmdi  27812  indifundif  27988  eulerpartlemt  29030  eulerpart  29041  ballotlem1  29145  ballotlemfval0  29154  ballotth  29196  subfaclim  29699  kur14lem6  29722  quad3  30090  iexpire  30158  pigt3  31642  volsupnfl  31689  areaquad  35800  wallispilem4  37499  dirkertrigeqlem3  37531  dirkercncflem1  37534  fourierswlem  37662  fouriersw  37663  tgoldbachlt  38299  3exp4mod41  38306  41prothprm  38309  zlmodzxz0  38897  linevalexample  38948