Theorem 3eqtr2i 2776

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

Syntax hints:   = wceq 1620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-ext 2728

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1842  df-cleq 2741

This theorem is referenced by:  indif  4000  dfrab3  4033  iunid  4715  cnvcnvOLD  5733  cocnvcnv2  5796  fmptap  6588  cnvoprab  7385  fpar  7437  fodomr  8264  jech9.3  8838  cda1dif  9161  alephadd  9562  distrnq  9946  ltanq  9956  ltrnq  9964  halfpm6th  11416  numma  11720  numaddc  11724  6p5lem  11758  8p2e10  11773  binom2i  13139  faclbnd4lem1  13245  cats2cat  13778  0.999...  14782  0.999...OLD  14783  flodddiv4  15310  6gcd4e2  15428  dfphi2  15652  mod2xnegi  15948  karatsuba  15965  karatsubaOLD  15966  1259lem1  16011  oppgtopn  17954  mgptopn  18669  ply1plusg  19768  ply1vsca  19769  ply1mulr  19770  restcld  21149  cmpsublem  21375  kgentopon  21514  txswaphmeolem  21780  dfii5  22860  itg1climres  23651  ang180lem1  24709  1cubrlem  24738  quart1lem  24752  efiatan  24809  log2cnv  24841  log2ublem3  24845  1sgm2ppw  25095  ppiub  25099  bposlem8  25186  bposlem9  25187  2lgsoddprmlem3c  25307  2lgsoddprmlem3d  25308  ax5seglem7  25985  2pthd  27031  3pthd  27297  ipidsq  27845  ipdirilem  27964  norm3difi  28284  polid2i  28294  pjclem3  29336  cvmdi  29463  indifundif  29634  dpmul  29901  eulerpartlemt  30713  eulerpart  30724  ballotlem1  30828  ballotlemfval0  30837  ballotth  30879  hgt750lem  31009  hgt750lem2  31010  subfaclim  31448  kur14lem6  31471  quad3  31842  iexpire  31899  pigt3  33684  volsupnfl  33736  dfxrn2  34430  xrninxp  34442  areaquad  38273  wallispilem4  40757  dirkertrigeqlem3  40789  dirkercncflem1  40792  fourierswlem  40919  fouriersw  40920  smflimsuplem8  41508  3exp4mod41  42012  41prothprm  42015  tgoldbachlt  42183  tgoldbachltOLD  42189  zlmodzxz0  42613  linevalexample  42663