Theorem 3eqtr2i 2768

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

Syntax hints:   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  indif  4208  dfrab3  4247  cocnvcnv2  6210  fmptap  7114  cnvoprab  8002  fpar  8055  fodomr  9056  fodomfir  9228  jech9.3  9729  dju1dif  10086  alephadd  10491  distrnq  10875  ltanq  10885  ltrnq  10893  1p2e3  12310  halfpm6th  12390  numma  12679  numaddc  12683  6p5lem  12705  8p2e10  12715  binom2i  14165  faclbnd4lem1  14246  cats2cat  14815  0.999...  15837  flodddiv4  16375  6gcd4e2  16498  dfphi2  16735  mod2xnegi  17033  karatsuba  17045  1259lem1  17092  setc2obas  18052  oppgtopn  19319  symgplusg  19349  cmnbascntr  19771  mgptopn  20120  ply1plusg  22208  ply1vsca  22209  ply1mulr  22210  restcld  23155  cmpsublem  23382  kgentopon  23521  dfii5  24870  itg1climres  25699  pigt3  26500  ang180lem1  26791  1cubrlem  26823  quart1lem  26837  efiatan  26894  log2cnv  26926  log2ublem3  26930  1sgm2ppw  27181  ppiub  27185  bposlem8  27272  bposlem9  27273  2lgsoddprmlem3c  27393  2lgsoddprmlem3d  27394  bday1  27824  addsasslem2  28014  seqsval  28298  ax5seglem7  29022  wlknwwlksnbij  29974  2pthd  30026  3pthd  30262  ipidsq  30799  ipdirilem  30918  norm3difi  31236  polid2i  31246  pjclem3  32286  cvmdi  32413  indifundif  32612  dpmul  32991  tocyccntz  33225  ccfldextdgrr  33856  cos9thpiminplylem5  33970  eulerpartlemt  34555  eulerpart  34566  ballotlem1  34671  ballotlemfval0  34680  ballotth  34722  hgt750lem  34835  hgt750lem2  34836  subfaclim  35416  kur14lem6  35439  quad3  35898  iexpire  35963  volsupnfl  38032  dfxrn2  38752  dmxrn  38754  dmxrnuncnvepres  38759  xrninxp  38782  1p3e4  42742  ipiiie0  42915  sn-0tie0  42941  areaquad  43661  wallispilem4  46511  dirkertrigeqlem3  46543  dirkercncflem1  46546  fourierswlem  46673  fouriersw  46674  smflimsuplem8  47270  ceil5half3  47809  3exp4mod41  48094  41prothprm  48097  tgoldbachlt  48307  zlmodzxz0  48847  linevalexample  48886  mndtcco  50075