Theorem 3eqtr2i 2758

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  indif  4239  dfrab3  4278  iunidOLD  5020  cocnvcnv2  6219  fmptap  7126  cnvoprab  8018  fpar  8072  fodomr  9069  fodomfir  9255  jech9.3  9743  dju1dif  10102  alephadd  10506  distrnq  10890  ltanq  10900  ltrnq  10908  1p2e3  12300  halfpm6th  12380  numma  12669  numaddc  12673  6p5lem  12695  8p2e10  12705  binom2i  14153  faclbnd4lem1  14234  cats2cat  14804  0.999...  15823  flodddiv4  16361  6gcd4e2  16484  dfphi2  16720  mod2xnegi  17018  karatsuba  17030  1259lem1  17077  setc2obas  18032  oppgtopn  19261  symgplusg  19289  cmnbascntr  19711  mgptopn  20033  ply1plusg  22084  ply1vsca  22085  ply1mulr  22086  restcld  23035  cmpsublem  23262  kgentopon  23401  dfii5  24754  itg1climres  25591  pigt3  26403  ang180lem1  26695  1cubrlem  26727  quart1lem  26741  efiatan  26798  log2cnv  26830  log2ublem3  26834  1sgm2ppw  27087  ppiub  27091  bposlem8  27178  bposlem9  27179  2lgsoddprmlem3c  27299  2lgsoddprmlem3d  27300  bday1s  27719  addsasslem2  27887  seqsval  28158  ax5seglem7  28838  wlknwwlksnbij  29791  2pthd  29843  3pthd  30076  ipidsq  30612  ipdirilem  30731  norm3difi  31049  polid2i  31059  pjclem3  32099  cvmdi  32226  indifundif  32426  dpmul  32806  tocyccntz  33074  ccfldextdgrr  33640  cos9thpiminplylem5  33749  eulerpartlemt  34335  eulerpart  34346  ballotlem1  34451  ballotlemfval0  34460  ballotth  34502  hgt750lem  34615  hgt750lem2  34616  subfaclim  35148  kur14lem6  35171  quad3  35630  iexpire  35695  volsupnfl  37632  dfxrn2  38331  dmxrn  38333  xrninxp  38351  1p3e4  42220  ipiiie0  42399  sn-0tie0  42412  areaquad  43178  wallispilem4  46039  dirkertrigeqlem3  46071  dirkercncflem1  46074  fourierswlem  46201  fouriersw  46202  smflimsuplem8  46798  ceil5half3  47314  3exp4mod41  47590  41prothprm  47593  tgoldbachlt  47790  zlmodzxz0  48317  linevalexample  48357  mndtcco  49547