Theorem 3eqtr2i 2798

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

Syntax hints:   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  indif  4241  dfrab3  4280  cocnvcnv2  6261  fmptap  7169  cnvoprab  8056  fpar  8110  fodomr  9115  fodomfir  9286  jech9.3  9785  dju1dif  10155  alephadd  10561  distrnq  10945  ltanq  10955  ltrnq  10963  1p2e3  12382  halfpm6th  12465  numma  12759  numaddc  12763  6p5lem  12785  8p2e10  12795  binom2i  14247  faclbnd4lem1  14328  cats2cat  14898  0.999...  15934  flodddiv4  16472  6gcd4e2  16595  dfphi2  16832  mod2xnegi  17130  karatsuba  17142  1259lem1  17190  setc2obas  18150  oppgtopn  19422  symgplusg  19452  cmnbascntr  19874  mgptopn  20223  ply1plusg  22351  ply1vsca  22352  ply1mulr  22353  restcld  23297  cmpsublem  23524  kgentopon  23663  dfii5  25012  itg1climres  25841  pigt3  26648  ang180lem1  26939  1cubrlem  26971  quart1lem  26985  efiatan  27042  log2cnv  27074  log2ublem3  27078  1sgm2ppw  27329  ppiub  27333  bposlem8  27420  bposlem9  27421  2lgsoddprmlem3c  27541  2lgsoddprmlem3d  27542  bday1  27972  addsasslem2  28162  seqsval  28446  ax5seglem7  29225  wlknwwlksnbij  30177  2pthd  30229  3pthd  30465  ipidsq  31002  ipdirilem  31121  norm3difi  31439  polid2i  31449  pjclem3  32489  cvmdi  32616  indifundif  32810  dpmul  33172  tocyccntz  33404  ccfldextdgrr  34006  cos9thpiminplylem5  34120  eulerpartlemt  34705  eulerpart  34716  ballotlem1  34821  ballotlemfval0  34830  ballotth  34872  hgt750lem  34982  hgt750lem2  34983  subfaclim  35578  kur14lem6  35601  quad3  36060  iexpire  36125  volsupnfl  38203  dfxrn2  38923  dmxrn  38925  dmxrnuncnvepres  38930  xrninxp  38953  1p3e4  42915  ipiiie0  43088  sn-0tie0  43114  areaquad  43834  wallispilem4  46673  dirkertrigeqlem3  46705  dirkercncflem1  46708  fourierswlem  46835  fouriersw  46836  smflimsuplem8  47432  ceil5half3  47971  3exp4mod41  48256  41prothprm  48259  tgoldbachlt  48469  zlmodzxz0  49020  linevalexample  49059  mndtcco  50247