Theorem 3eqtr2i 2451

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 2448	. 2 |- A = C
4		3eqtr2i.3	. 2 |- C = D
5	3, 4	eqtri 2445	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 1663  ax-4 1676  ax-ext 2403

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

This theorem is referenced by:  indif  3653  dfrab3  3686  iunid  4292  cnvcnv  5245  cocnvcnv2  5304  fmptap  6041  fpar  6850  fodomr  7671  jech9.3  8232  cda1dif  8552  alephadd  8948  distrnq  9332  ltanq  9342  ltrnq  9350  negdiiOLD  9905  halfpm6th  10780  numma  11028  numaddc  11032  6p5lem  11046  binom2i  12329  faclbnd4lem1  12423  0.999...  13875  6gcd4e2  14440  dfphi2  14660  mod2xnegi  14981  karatsuba  14994  1259lem1  15040  oppgtopn  16942  mgptopn  17670  ply1plusg  18756  ply1vsca  18757  ply1mulr  18758  restcld  20125  cmpsublem  20351  kgentopon  20490  txswaphmeolem  20756  dfii5  21854  itg1climres  22609  ang180lem1  23675  1cubrlem  23704  quart1lem  23718  efiatan  23775  log2cnv  23807  1sgm2ppw  24065  ppiub  24069  bposlem8  24156  bposlem9  24157  ax5seglem7  24902  usgraexmplcvtx  25070  usgraexmplcedg  25071  ipidsq  26286  ipdirilem  26407  norm3difi  26737  polid2i  26747  pjclem3  27787  cvmdi  27914  indifundif  28090  eulerpartlemt  29151  eulerpart  29162  ballotlem1  29266  ballotlemfval0  29275  ballotth  29317  ballotthOLD  29355  subfaclim  29858  kur14lem6  29881  quad3  30249  iexpire  30317  pigt3  31845  volsupnfl  31892  areaquad  36014  wallispilem4  37813  dirkertrigeqlem3  37845  dirkercncflem1  37848  fourierswlem  37977  fouriersw  37978  tgoldbachlt  38722  3exp4mod41  38729  41prothprm  38732  zlmodzxz0  39730  linevalexample  39781