Theorem 3eqtr2i 2791

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

Syntax hints:   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  indif  4232  dfrab3  4271  cocnvcnv2  6246  fmptap  7154  cnvoprab  8041  fpar  8095  fodomr  9100  fodomfir  9272  jech9.3  9772  dju1dif  10129  alephadd  10535  distrnq  10919  ltanq  10929  ltrnq  10937  1p2e3  12360  halfpm6th  12443  numma  12737  numaddc  12741  6p5lem  12763  8p2e10  12773  binom2i  14225  faclbnd4lem1  14306  cats2cat  14875  0.999...  15911  flodddiv4  16449  6gcd4e2  16572  dfphi2  16809  mod2xnegi  17107  karatsuba  17119  1259lem1  17167  setc2obas  18127  oppgtopn  19393  symgplusg  19423  cmnbascntr  19845  mgptopn  20194  ply1plusg  22282  ply1vsca  22283  ply1mulr  22284  restcld  23229  cmpsublem  23456  kgentopon  23595  dfii5  24944  itg1climres  25773  pigt3  26580  ang180lem1  26871  1cubrlem  26903  quart1lem  26917  efiatan  26974  log2cnv  27006  log2ublem3  27010  1sgm2ppw  27261  ppiub  27265  bposlem8  27352  bposlem9  27353  2lgsoddprmlem3c  27473  2lgsoddprmlem3d  27474  bday1  27904  addsasslem2  28094  seqsval  28378  ax5seglem7  29133  wlknwwlksnbij  30085  2pthd  30137  3pthd  30373  ipidsq  30910  ipdirilem  31029  norm3difi  31347  polid2i  31357  pjclem3  32397  cvmdi  32524  indifundif  32720  dpmul  33087  tocyccntz  33321  ccfldextdgrr  33966  cos9thpiminplylem5  34080  eulerpartlemt  34665  eulerpart  34676  ballotlem1  34781  ballotlemfval0  34790  ballotth  34832  hgt750lem  34942  hgt750lem2  34943  subfaclim  35535  kur14lem6  35558  quad3  36017  iexpire  36082  volsupnfl  38161  dfxrn2  38881  dmxrn  38883  dmxrnuncnvepres  38888  xrninxp  38911  1p3e4  42871  ipiiie0  43044  sn-0tie0  43070  areaquad  43790  wallispilem4  46639  dirkertrigeqlem3  46671  dirkercncflem1  46674  fourierswlem  46801  fouriersw  46802  smflimsuplem8  47398  ceil5half3  47937  3exp4mod41  48222  41prothprm  48225  tgoldbachlt  48435  zlmodzxz0  48975  linevalexample  49014  mndtcco  50203