Theorem 3eqtr2i 2766

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

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

This theorem is referenced by:  indif  4234  dfrab3  4273  cocnvcnv2  6225  fmptap  7126  cnvoprab  8014  fpar  8068  fodomr  9068  fodomfir  9240  jech9.3  9738  dju1dif  10095  alephadd  10500  distrnq  10884  ltanq  10894  ltrnq  10902  1p2e3  12295  halfpm6th  12375  numma  12663  numaddc  12667  6p5lem  12689  8p2e10  12699  binom2i  14147  faclbnd4lem1  14228  cats2cat  14797  0.999...  15816  flodddiv4  16354  6gcd4e2  16477  dfphi2  16713  mod2xnegi  17011  karatsuba  17023  1259lem1  17070  setc2obas  18030  oppgtopn  19294  symgplusg  19324  cmnbascntr  19746  mgptopn  20095  ply1plusg  22176  ply1vsca  22177  ply1mulr  22178  restcld  23128  cmpsublem  23355  kgentopon  23494  dfii5  24846  itg1climres  25683  pigt3  26495  ang180lem1  26787  1cubrlem  26819  quart1lem  26833  efiatan  26890  log2cnv  26922  log2ublem3  26926  1sgm2ppw  27179  ppiub  27183  bposlem8  27270  bposlem9  27271  2lgsoddprmlem3c  27391  2lgsoddprmlem3d  27392  bday1  27822  addsasslem2  28012  seqsval  28296  ax5seglem7  29020  wlknwwlksnbij  29973  2pthd  30025  3pthd  30261  ipidsq  30798  ipdirilem  30917  norm3difi  31235  polid2i  31245  pjclem3  32285  cvmdi  32412  indifundif  32611  dpmul  33005  tocyccntz  33238  ccfldextdgrr  33850  cos9thpiminplylem5  33964  eulerpartlemt  34549  eulerpart  34560  ballotlem1  34665  ballotlemfval0  34674  ballotth  34716  hgt750lem  34829  hgt750lem2  34830  subfaclim  35404  kur14lem6  35427  quad3  35886  iexpire  35951  volsupnfl  37916  dfxrn2  38636  dmxrn  38638  dmxrnuncnvepres  38643  xrninxp  38666  1p3e4  42629  ipiiie0  42808  sn-0tie0  42821  areaquad  43573  wallispilem4  46426  dirkertrigeqlem3  46458  dirkercncflem1  46461  fourierswlem  46588  fouriersw  46589  smflimsuplem8  47185  ceil5half3  47700  3exp4mod41  47976  41prothprm  47979  tgoldbachlt  48176  zlmodzxz0  48716  linevalexample  48755  mndtcco  49944