Theorem 3eqtr2i 2793

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

Syntax hints:   = wceq 1652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758

This theorem is referenced by:  indif  4036  dfrab3  4068  iunid  4733  cnvcnvOLD  5772  cocnvcnv2  5835  fmptap  6633  cnvoprab  7434  fpar  7487  fodomr  8322  jech9.3  8896  cda1dif  9255  alephadd  9656  distrnq  10040  ltanq  10050  ltrnq  10058  halfpm6th  11503  numma  11790  numaddc  11794  6p5lem  11816  8p2e10  11826  binom2i  13186  faclbnd4lem1  13289  cats2cat  13905  0.999...  14910  flodddiv4  15432  6gcd4e2  15550  dfphi2  15772  mod2xnegi  16068  karatsuba  16081  1259lem1  16125  oppgtopn  18060  mgptopn  18779  ply1plusg  19882  ply1vsca  19883  ply1mulr  19884  restcld  21270  cmpsublem  21496  kgentopon  21635  txswaphmeolem  21901  dfii5  22981  itg1climres  23786  ang180lem1  24844  1cubrlem  24873  quart1lem  24887  efiatan  24944  log2cnv  24976  log2ublem3  24980  1sgm2ppw  25230  ppiub  25234  bposlem8  25321  bposlem9  25322  2lgsoddprmlem3c  25442  2lgsoddprmlem3d  25443  ax5seglem7  26120  wlknwwlksnbij  27102  2pthd  27181  3pthd  27470  ipidsq  28042  ipdirilem  28161  norm3difi  28481  polid2i  28491  pjclem3  29533  cvmdi  29660  indifundif  29826  dpmul  30089  eulerpartlemt  30901  eulerpart  30912  ballotlem1  31017  ballotlemfval0  31026  ballotth  31068  hgt750lem  31201  hgt750lem2  31202  subfaclim  31639  kur14lem6  31662  quad3  32031  iexpire  32087  pigt3  33847  volsupnfl  33899  dfxrn2  34588  xrninxp  34600  areaquad  38502  wallispilem4  40946  dirkertrigeqlem3  40978  dirkercncflem1  40981  fourierswlem  41108  fouriersw  41109  smflimsuplem8  41697  3exp4mod41  42233  41prothprm  42236  tgoldbachlt  42404  zlmodzxz0  42827  linevalexample  42877