Theorem 3eqtr2i 2469

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

Syntax hints:   = wceq 1369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436

This theorem is referenced by:  indif  3613  dfrab3  3646  iunid  4246  cnvcnv  5311  cocnvcnv2  5370  fmptap  5922  fpar  6697  fodomr  7483  jech9.3  8042  cda1dif  8366  alephadd  8762  distrnq  9151  ltanq  9161  ltrnq  9169  negdii  9713  halfpm6th  10567  numma  10807  numaddc  10811  6p5lem  10825  binom2i  11996  faclbnd4lem1  12090  0.999...  13362  dfphi2  13870  mod2xnegi  14121  karatsuba  14134  1259lem1  14176  oppgtopn  15889  mgptopn  16622  ply1plusg  17701  ply1vsca  17702  ply1mulr  17703  restcld  18798  cmpsublem  19024  kgentopon  19133  txswaphmeolem  19399  dfii5  20483  itg1climres  21214  ang180lem1  22227  1cubrlem  22258  quart1lem  22272  efiatan  22329  log2cnv  22361  1sgm2ppw  22561  ppiub  22565  bposlem8  22652  bposlem9  22653  ax5seglem7  23203  ipidsq  24130  ipdirilem  24251  norm3difi  24571  polid2i  24581  pjclem3  25623  cvmdi  25750  eulerpartlemt  26776  ballotlem1  26891  ballotlemfval0  26900  ballotth  26942  subfaclim  27098  kur14lem6  27121  volsupnfl  28462  areaquad  29618  wallispilem4  29889  zlmodzxz0  30782  linevalexample  30892