Theorem 3eqtr2i 2461

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

Syntax hints:   = wceq 1364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-12 1793  ax-ext 2416

This theorem depends on definitions:  df-bi 185  df-ex 1592  df-cleq 2428

This theorem is referenced by:  indif  3582  dfrab3  3615  iunid  4215  cnvcnv  5280  cocnvcnv2  5339  fmptap  5890  fpar  6667  fodomr  7452  jech9.3  8011  cda1dif  8335  alephadd  8731  distrnq  9120  ltanq  9130  ltrnq  9138  negdii  9682  halfpm6th  10536  numma  10776  numaddc  10780  6p5lem  10794  binom2i  11961  faclbnd4lem1  12055  0.999...  13326  dfphi2  13834  mod2xnegi  14085  karatsuba  14098  1259lem1  14140  oppgtopn  15850  mgptopn  16576  ply1plusg  17580  ply1vsca  17581  ply1mulr  17582  restcld  18620  cmpsublem  18846  kgentopon  18955  txswaphmeolem  19221  dfii5  20305  itg1climres  21036  ang180lem1  22092  1cubrlem  22123  quart1lem  22137  efiatan  22194  log2cnv  22226  1sgm2ppw  22426  ppiub  22430  bposlem8  22517  bposlem9  22518  ax5seglem7  23006  ipidsq  23933  ipdirilem  24054  norm3difi  24374  polid2i  24384  pjclem3  25426  cvmdi  25553  eulerpartlemt  26604  eulerpart  26615  ballotlem1  26719  ballotlemfval0  26728  ballotth  26770  subfaclim  26926  kur14lem6  26949  volsupnfl  28282  wallispilem4  29711  zlmodzxz0  30590  linevalexample  30649