Theorem 3eqtr2i 2492

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 2489	. 2
4		3eqtr2i.3	. 2
5	3, 4	eqtri 2486	1

Syntax hints:  =wceq 1395

This theorem is referenced by:  indif  3739  dfrab3  3772  iunid  4385  cnvcnv  5464  cocnvcnv2  5524  fmptap  6094  fpar  6904  fodomr  7688  jech9.3  8253  cda1dif  8577  alephadd  8973  distrnq  9360  ltanq  9370  ltrnq  9378  negdiiOLD  9927  halfpm6th  10785  numma  11035  numaddc  11039  6p5lem  11053  binom2i  12277  faclbnd4lem1  12371  0.999...  13690  dfphi2  14304  mod2xnegi  14557  karatsuba  14570  1259lem1  14613  oppgtopn  16388  mgptopn  17150  ply1plusg  18266  ply1vsca  18267  ply1mulr  18268  restcld  19673  cmpsublem  19899  kgentopon  20039  txswaphmeolem  20305  dfii5  21389  itg1climres  22121  ang180lem1  23141  1cubrlem  23172  quart1lem  23186  efiatan  23243  log2cnv  23275  1sgm2ppw  23475  ppiub  23479  bposlem8  23566  bposlem9  23567  ax5seglem7  24238  usgraexmplcvtx  24405  usgraexmplcedg  24406  ipidsq  25623  ipdirilem  25744  norm3difi  26064  polid2i  26074  pjclem3  27116  cvmdi  27243  eulerpartlemt  28310  eulerpart  28321  ballotlem1  28425  ballotlemfval0  28434  ballotth  28476  subfaclim  28632  kur14lem6  28655  quad3  29024  iexpire  29122  volsupnfl  30059  areaquad  31184  wallispilem4  31850  dirkertrigeqlem3  31882  dirkercncflem1  31885  fourierswlem  32013  fouriersw  32014  zlmodzxz0  32945  linevalexample  32996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-cleq 2449