Theorem 3eqtr2i 2649

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

Hypotheses

Ref	Expression
3eqtr2i.1	⊢ 𝐴 = 𝐵
3eqtr2i.2	⊢ 𝐶 = 𝐵
3eqtr2i.3	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
3eqtr2i	⊢ 𝐴 = 𝐷

Proof of Theorem 3eqtr2i

Step	Hyp	Ref	Expression
1		3eqtr2i.1	. . 3 ⊢ 𝐴 = 𝐵
2		3eqtr2i.2	. . 3 ⊢ 𝐶 = 𝐵
3	1, 2	eqtr4i 2646	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtri 2643	1 ⊢ 𝐴 = 𝐷

Syntax hints:   = wceq 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614

This theorem is referenced by:  indif  3851  dfrab3  3884  iunid  4548  cnvcnvOLD  5556  cocnvcnv2  5616  fmptap  6401  fpar  7241  fodomr  8071  jech9.3  8637  cda1dif  8958  alephadd  9359  distrnq  9743  ltanq  9753  ltrnq  9761  halfpm6th  11213  numma  11517  numaddc  11521  6p5lem  11555  8p2e10  11570  binom2i  12930  faclbnd4lem1  13036  cats2cat  13560  0.999...  14556  0.999...OLD  14557  flodddiv4  15080  6gcd4e2  15198  dfphi2  15422  mod2xnegi  15718  karatsuba  15735  karatsubaOLD  15736  1259lem1  15781  oppgtopn  17723  mgptopn  18438  ply1plusg  19535  ply1vsca  19536  ply1mulr  19537  restcld  20916  cmpsublem  21142  kgentopon  21281  txswaphmeolem  21547  dfii5  22628  itg1climres  23421  ang180lem1  24473  1cubrlem  24502  quart1lem  24516  efiatan  24573  log2cnv  24605  log2ublem3  24609  1sgm2ppw  24859  ppiub  24863  bposlem8  24950  bposlem9  24951  2lgsoddprmlem3c  25071  2lgsoddprmlem3d  25072  ax5seglem7  25749  2pthd  26739  3pthd  26934  ipidsq  27453  ipdirilem  27572  norm3difi  27892  polid2i  27902  pjclem3  28944  cvmdi  29071  indifundif  29244  eulerpartlemt  30256  eulerpart  30267  ballotlem1  30371  ballotlemfval0  30380  ballotth  30422  subfaclim  30931  kur14lem6  30954  quad3  31325  iexpire  31382  pigt3  33073  volsupnfl  33125  areaquad  37322  wallispilem4  39622  dirkertrigeqlem3  39654  dirkercncflem1  39657  fourierswlem  39784  fouriersw  39785  smflimsuplem8  40370  3exp4mod41  40862  41prothprm  40865  tgoldbachlt  41021  tgoldbachltOLD  41028  zlmodzxz0  41452  linevalexample  41502