Theorem 3eqtr2i 2765

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

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  indif  4232  dfrab3  4271  cocnvcnv2  6217  fmptap  7116  cnvoprab  8004  fpar  8058  fodomr  9056  fodomfir  9228  jech9.3  9726  dju1dif  10083  alephadd  10488  distrnq  10872  ltanq  10882  ltrnq  10890  1p2e3  12283  halfpm6th  12363  numma  12651  numaddc  12655  6p5lem  12677  8p2e10  12687  binom2i  14135  faclbnd4lem1  14216  cats2cat  14785  0.999...  15804  flodddiv4  16342  6gcd4e2  16465  dfphi2  16701  mod2xnegi  16999  karatsuba  17011  1259lem1  17058  setc2obas  18018  oppgtopn  19282  symgplusg  19312  cmnbascntr  19734  mgptopn  20083  ply1plusg  22164  ply1vsca  22165  ply1mulr  22166  restcld  23116  cmpsublem  23343  kgentopon  23482  dfii5  24834  itg1climres  25671  pigt3  26483  ang180lem1  26775  1cubrlem  26807  quart1lem  26821  efiatan  26878  log2cnv  26910  log2ublem3  26914  1sgm2ppw  27167  ppiub  27171  bposlem8  27258  bposlem9  27259  2lgsoddprmlem3c  27379  2lgsoddprmlem3d  27380  bday1  27810  addsasslem2  28000  seqsval  28284  ax5seglem7  29008  wlknwwlksnbij  29961  2pthd  30013  3pthd  30249  ipidsq  30785  ipdirilem  30904  norm3difi  31222  polid2i  31232  pjclem3  32272  cvmdi  32399  indifundif  32599  dpmul  32994  tocyccntz  33226  ccfldextdgrr  33829  cos9thpiminplylem5  33943  eulerpartlemt  34528  eulerpart  34539  ballotlem1  34644  ballotlemfval0  34653  ballotth  34695  hgt750lem  34808  hgt750lem2  34809  subfaclim  35382  kur14lem6  35405  quad3  35864  iexpire  35929  volsupnfl  37866  dfxrn2  38570  dmxrn  38572  dmxrnuncnvepres  38577  xrninxp  38600  1p3e4  42514  ipiiie0  42693  sn-0tie0  42706  areaquad  43458  wallispilem4  46312  dirkertrigeqlem3  46344  dirkercncflem1  46347  fourierswlem  46474  fouriersw  46475  smflimsuplem8  47071  ceil5half3  47586  3exp4mod41  47862  41prothprm  47865  tgoldbachlt  48062  zlmodzxz0  48602  linevalexample  48641  mndtcco  49830