Theorem 3eqtr2i 2638

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 2635	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtri 2632	1 ⊢ 𝐴 = 𝐷

Syntax hints:   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  indif  3828  dfrab3  3861  iunid  4511  cnvcnv  5505  cocnvcnv2  5564  fmptap  6341  fpar  7168  fodomr  7996  jech9.3  8560  cda1dif  8881  alephadd  9278  distrnq  9662  ltanq  9672  ltrnq  9680  halfpm6th  11130  numma  11433  numaddc  11437  6p5lem  11471  8p2e10  11486  binom2i  12836  faclbnd4lem1  12942  cats2cat  13458  0.999...  14451  0.999...OLD  14452  flodddiv4  14975  6gcd4e2  15093  dfphi2  15317  mod2xnegi  15613  karatsuba  15630  karatsubaOLD  15631  1259lem1  15676  oppgtopn  17606  mgptopn  18321  ply1plusg  19416  ply1vsca  19417  ply1mulr  19418  restcld  20786  cmpsublem  21012  kgentopon  21151  txswaphmeolem  21417  dfii5  22496  itg1climres  23287  ang180lem1  24339  1cubrlem  24368  quart1lem  24382  efiatan  24439  log2cnv  24471  log2ublem3  24475  1sgm2ppw  24725  ppiub  24729  bposlem8  24816  bposlem9  24817  2lgsoddprmlem3c  24937  2lgsoddprmlem3d  24938  ax5seglem7  25615  usgraexmplcvtx  25934  usgraexmplcedg  25935  ipidsq  26949  ipdirilem  27068  norm3difi  27388  polid2i  27398  pjclem3  28440  cvmdi  28567  indifundif  28740  eulerpartlemt  29760  eulerpart  29771  ballotlem1  29875  ballotlemfval0  29884  ballotth  29926  subfaclim  30424  kur14lem6  30447  quad3  30818  iexpire  30874  pigt3  32572  volsupnfl  32624  areaquad  36821  wallispilem4  38961  dirkertrigeqlem3  38993  dirkercncflem1  38996  fourierswlem  39123  fouriersw  39124  3exp4mod41  40071  41prothprm  40074  tgoldbachlt  40230  tgoldbachltOLD  40237  2pthd  41147  3pthd  41341  zlmodzxz0  41927  linevalexample  41978