Theorem 3eqtr2i 2790

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  indif  4226  dfrab3  4265  cocnvcnv2  6259  fmptap  7173  cnvoprab  8069  fpar  8125  fodomr  9140  fodomfir  9312  jech9.3OLD  9816  dju1dif  10244  alephadd  10655  distrnq  11039  ltanq  11049  ltrnq  11057  1p2e3  12478  halfpm6th  12561  numma  12856  numaddc  12860  6p5lem  12882  8p2e10  12892  binom2i  14349  faclbnd4lem1  14430  cats2cat  15006  0.999...  16043  flodddiv4  16578  6gcd4e2  16704  dfphi2  16944  mod2xnegi  17242  karatsuba  17254  1259lem1  17302  setc2obas  18262  oppgtopn  19560  symgplusg  19590  cmnbascntr  20012  mgptopn  20361  ply1plusg  22534  ply1vsca  22535  ply1mulr  22536  restcld  23483  cmpsublem  23710  kgentopon  23850  dfii5  25199  itg1climres  26028  pigt3  26839  ang180lem1  27130  1cubrlem  27162  quart1lem  27176  efiatan  27233  log2cnv  27265  log2ublem3  27269  1sgm2ppw  27520  ppiub  27524  bposlem8  27611  bposlem9  27612  2lgsoddprmlem3c  27732  2lgsoddprmlem3d  27733  bday1  28193  addsasslem2  28383  seqsval  28667  ax5seglem7  29506  wlknwwlksnbij  30470  2pthd  30522  3pthd  30768  ipidsq  31305  ipdirilem  31424  norm3difi  31742  polid2i  31752  pjclem3  32792  cvmdi  32919  indifundif  33113  dpmul  33472  tocyccntz  33698  ccfldextdgrr  34297  cos9thpiminplylem5  34411  eulerpartlemt  34996  eulerpart  35007  ballotlem1  35112  ballotlemfval0  35121  ballotth  35163  hgt750lem  35273  hgt750lem2  35274  subfaclim  35932  kur14lem6  35955  quad3  36414  iexpire  36479  volsupnfl  38563  dfxrn2  39297  dmxrn  39299  dmxrnuncnvepres  39304  xrninxp  39327  1p3e4  43290  1p4e5  43291  1p5e6  43292  1p6e7  43293  1p7e8  43294  1p8e9  43295  4p5e9  43304  ipiiie0  43469  sn-0tie0  43495  areaquad  44202  wallispilem4  47047  dirkertrigeqlem3  47079  dirkercncflem1  47082  fourierswlem  47209  fouriersw  47210  smflimsuplem8  47806  goldpolyfactor  47896  ceil5half3  48385  3exp4mod41  48670  41prothprm  48673  tgoldbachlt  48883  zlmodzxz0  49437  linevalexample  49476  mndtcco  50662