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 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  indif  4220  dfrab3  4259  cocnvcnv2  6223  fmptap  7125  cnvoprab  8013  fpar  8066  fodomr  9066  fodomfir  9238  jech9.3  9738  dju1dif  10095  alephadd  10500  distrnq  10884  ltanq  10894  ltrnq  10902  1p2e3  12319  halfpm6th  12399  numma  12688  numaddc  12692  6p5lem  12714  8p2e10  12724  binom2i  14174  faclbnd4lem1  14255  cats2cat  14824  0.999...  15846  flodddiv4  16384  6gcd4e2  16507  dfphi2  16744  mod2xnegi  17042  karatsuba  17054  1259lem1  17101  setc2obas  18061  oppgtopn  19328  symgplusg  19358  cmnbascntr  19780  mgptopn  20129  ply1plusg  22187  ply1vsca  22188  ply1mulr  22189  restcld  23137  cmpsublem  23364  kgentopon  23503  dfii5  24852  itg1climres  25681  pigt3  26482  ang180lem1  26773  1cubrlem  26805  quart1lem  26819  efiatan  26876  log2cnv  26908  log2ublem3  26912  1sgm2ppw  27163  ppiub  27167  bposlem8  27254  bposlem9  27255  2lgsoddprmlem3c  27375  2lgsoddprmlem3d  27376  bday1  27806  addsasslem2  27996  seqsval  28280  ax5seglem7  29004  wlknwwlksnbij  29956  2pthd  30008  3pthd  30244  ipidsq  30781  ipdirilem  30900  norm3difi  31218  polid2i  31228  pjclem3  32268  cvmdi  32395  indifundif  32594  dpmul  32972  tocyccntz  33205  ccfldextdgrr  33816  cos9thpiminplylem5  33930  eulerpartlemt  34515  eulerpart  34526  ballotlem1  34631  ballotlemfval0  34640  ballotth  34682  hgt750lem  34795  hgt750lem2  34796  subfaclim  35370  kur14lem6  35393  quad3  35852  iexpire  35917  volsupnfl  37986  dfxrn2  38706  dmxrn  38708  dmxrnuncnvepres  38713  xrninxp  38736  1p3e4  42697  ipiiie0  42870  sn-0tie0  42896  areaquad  43644  wallispilem4  46496  dirkertrigeqlem3  46528  dirkercncflem1  46531  fourierswlem  46658  fouriersw  46659  smflimsuplem8  47255  ceil5half3  47794  3exp4mod41  48079  41prothprm  48082  tgoldbachlt  48292  zlmodzxz0  48832  linevalexample  48871  mndtcco  50060