Theorem 3eqtr2i 2850

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

Syntax hints:   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814

This theorem is referenced by:  indif  4245  dfrab3  4277  iunid  4983  cocnvcnv2  6110  fmptap  6931  cnvoprab  7757  fpar  7810  fodomr  8667  jech9.3  9242  dju1dif  9597  alephadd  9998  distrnq  10382  ltanq  10392  ltrnq  10400  1p2e3  11779  halfpm6th  11857  numma  12141  numaddc  12145  6p5lem  12167  8p2e10  12177  binom2i  13573  faclbnd4lem1  13652  cats2cat  14223  0.999...  15236  flodddiv4  15763  6gcd4e2  15885  dfphi2  16110  mod2xnegi  16406  karatsuba  16419  1259lem1  16463  oppgtopn  18480  symgplusg  18510  mgptopn  19247  ply1plusg  20392  ply1vsca  20393  ply1mulr  20394  restcld  21779  cmpsublem  22006  kgentopon  22145  dfii5  23492  itg1climres  24314  pigt3  25102  ang180lem1  25386  1cubrlem  25418  quart1lem  25432  efiatan  25489  log2cnv  25521  log2ublem3  25525  1sgm2ppw  25775  ppiub  25779  bposlem8  25866  bposlem9  25867  2lgsoddprmlem3c  25987  2lgsoddprmlem3d  25988  ax5seglem7  26720  wlknwwlksnbij  27665  2pthd  27718  3pthd  27952  ipidsq  28486  ipdirilem  28605  norm3difi  28923  polid2i  28933  pjclem3  29973  cvmdi  30100  indifundif  30284  dpmul  30589  tocyccntz  30786  ccfldextdgrr  31057  eulerpartlemt  31629  eulerpart  31640  ballotlem1  31744  ballotlemfval0  31753  ballotth  31795  hgt750lem  31922  hgt750lem2  31923  subfaclim  32435  kur14lem6  32458  quad3  32913  iexpire  32967  volsupnfl  34936  dfxrn2  35627  xrninxp  35639  areaquad  39821  wallispilem4  42352  dirkertrigeqlem3  42384  dirkercncflem1  42387  fourierswlem  42514  fouriersw  42515  smflimsuplem8  43100  3exp4mod41  43780  41prothprm  43783  tgoldbachlt  43980  zlmodzxz0  44403  linevalexample  44449