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  4231  dfrab3  4270  iunidOLD  5010  cocnvcnv2  6207  fmptap  7106  cnvoprab  7995  fpar  8049  fodomr  9045  fodomfir  9218  jech9.3  9710  dju1dif  10067  alephadd  10471  distrnq  10855  ltanq  10865  ltrnq  10873  1p2e3  12266  halfpm6th  12346  numma  12635  numaddc  12639  6p5lem  12661  8p2e10  12671  binom2i  14119  faclbnd4lem1  14200  cats2cat  14769  0.999...  15788  flodddiv4  16326  6gcd4e2  16449  dfphi2  16685  mod2xnegi  16983  karatsuba  16995  1259lem1  17042  setc2obas  18001  oppgtopn  19232  symgplusg  19262  cmnbascntr  19684  mgptopn  20033  ply1plusg  22106  ply1vsca  22107  ply1mulr  22108  restcld  23057  cmpsublem  23284  kgentopon  23423  dfii5  24776  itg1climres  25613  pigt3  26425  ang180lem1  26717  1cubrlem  26749  quart1lem  26763  efiatan  26820  log2cnv  26852  log2ublem3  26856  1sgm2ppw  27109  ppiub  27113  bposlem8  27200  bposlem9  27201  2lgsoddprmlem3c  27321  2lgsoddprmlem3d  27322  bday1s  27745  addsasslem2  27916  seqsval  28187  ax5seglem7  28880  wlknwwlksnbij  29833  2pthd  29885  3pthd  30118  ipidsq  30654  ipdirilem  30773  norm3difi  31091  polid2i  31101  pjclem3  32141  cvmdi  32268  indifundif  32468  dpmul  32853  tocyccntz  33086  ccfldextdgrr  33639  cos9thpiminplylem5  33753  eulerpartlemt  34339  eulerpart  34350  ballotlem1  34455  ballotlemfval0  34464  ballotth  34506  hgt750lem  34619  hgt750lem2  34620  subfaclim  35161  kur14lem6  35184  quad3  35643  iexpire  35708  volsupnfl  37645  dfxrn2  38344  dmxrn  38346  xrninxp  38364  1p3e4  42232  ipiiie0  42411  sn-0tie0  42424  areaquad  43189  wallispilem4  46049  dirkertrigeqlem3  46081  dirkercncflem1  46084  fourierswlem  46211  fouriersw  46212  smflimsuplem8  46808  ceil5half3  47324  3exp4mod41  47600  41prothprm  47603  tgoldbachlt  47800  zlmodzxz0  48340  linevalexample  48380  mndtcco  49570