Theorem 3eqtr2i 2763

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 2760	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtri 2757	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 2706

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

This theorem is referenced by:  indif  4230  dfrab3  4269  cocnvcnv2  6215  fmptap  7114  cnvoprab  8002  fpar  8056  fodomr  9054  fodomfir  9226  jech9.3  9724  dju1dif  10081  alephadd  10486  distrnq  10870  ltanq  10880  ltrnq  10888  1p2e3  12281  halfpm6th  12361  numma  12649  numaddc  12653  6p5lem  12675  8p2e10  12685  binom2i  14133  faclbnd4lem1  14214  cats2cat  14783  0.999...  15802  flodddiv4  16340  6gcd4e2  16463  dfphi2  16699  mod2xnegi  16997  karatsuba  17009  1259lem1  17056  setc2obas  18016  oppgtopn  19280  symgplusg  19310  cmnbascntr  19732  mgptopn  20081  ply1plusg  22162  ply1vsca  22163  ply1mulr  22164  restcld  23114  cmpsublem  23341  kgentopon  23480  dfii5  24832  itg1climres  25669  pigt3  26481  ang180lem1  26773  1cubrlem  26805  quart1lem  26819  efiatan  26876  log2cnv  26908  log2ublem3  26912  1sgm2ppw  27165  ppiub  27169  bposlem8  27256  bposlem9  27257  2lgsoddprmlem3c  27377  2lgsoddprmlem3d  27378  bday1s  27802  addsasslem2  27974  seqsval  28249  ax5seglem7  28957  wlknwwlksnbij  29910  2pthd  29962  3pthd  30198  ipidsq  30734  ipdirilem  30853  norm3difi  31171  polid2i  31181  pjclem3  32221  cvmdi  32348  indifundif  32548  dpmul  32943  tocyccntz  33175  ccfldextdgrr  33778  cos9thpiminplylem5  33892  eulerpartlemt  34477  eulerpart  34488  ballotlem1  34593  ballotlemfval0  34602  ballotth  34644  hgt750lem  34757  hgt750lem2  34758  subfaclim  35331  kur14lem6  35354  quad3  35813  iexpire  35878  volsupnfl  37805  dfxrn2  38509  dmxrn  38511  dmxrnuncnvepres  38516  xrninxp  38539  1p3e4  42456  ipiiie0  42635  sn-0tie0  42648  areaquad  43400  wallispilem4  46254  dirkertrigeqlem3  46286  dirkercncflem1  46289  fourierswlem  46416  fouriersw  46417  smflimsuplem8  47013  ceil5half3  47528  3exp4mod41  47804  41prothprm  47807  tgoldbachlt  48004  zlmodzxz0  48544  linevalexample  48583  mndtcco  49772