Theorem 3eqtr3i 2494

Description: An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr3i.1
3eqtr3i.2
3eqtr3i.3

Assertion

Ref	Expression
3eqtr3i

Proof of Theorem 3eqtr3i

Step	Hyp	Ref	Expression
1		3eqtr3i.1	. . 3
2		3eqtr3i.2	. . 3
3	1, 2	eqtr3i 2488	. 2
4		3eqtr3i.3	. 2
5	3, 4	eqtr3i 2488	1

Syntax hints:  =wceq 1395

This theorem is referenced by:  un12  3661  in12  3708  indif1  3741  difundi  3749  difundir  3750  difindi  3751  difindir  3752  dif32  3760  csbvarg  3848  undif1  3903  resmpt3  5329  xp0  5430  fresaunres2  5762  fvsnun1  6106  caov12  6503  caov13  6505  caov411  6507  caovdir  6509  orduniss2  6668  fparlem3  6902  fparlem4  6903  hartogslem1  7988  kmlem3  8553  cdaassen  8583  xpcdaen  8584  halfnq  9375  reclem3pr  9448  addcmpblnr  9467  ltsrpr  9475  pn0sr  9499  sqgt0sr  9504  map2psrpr  9508  negsubdii  9928  halfpm6th  10785  i4  12270  nn0opthlem1  12348  fac4  12361  imi  12990  ef01bndlem  13919  bitsres  14123  gcdaddmlem  14166  modsubi  14558  gcdmodi  14560  numexpp1  14564  karatsuba  14570  oppgcntr  16400  frgpuplem  16790  ressmpladd  18119  ressmplmul  18120  ressmplvsca  18121  ltbwe  18137  ressply1add  18271  ressply1mul  18272  ressply1vsca  18273  sn0cld  19591  qtopres  20199  itg1addlem5  22107  cospi  22865  sincos4thpi  22906  sincos3rdpi  22909  dvlog  23032  dvlog2  23034  dvsqrt  23118  ang180lem3  23143  1cubrlem  23172  mcubic  23178  quart1lem  23186  atantayl2  23269  log2cnv  23275  log2ublem2  23278  log2ub  23280  chtub  23487  bclbnd  23555  bposlem8  23566  lgsdir2lem1  23598  lgsdir2lem5  23602  ipidsq  25623  ip1ilem  25741  ipdirilem  25744  ipasslem10  25754  siilem1  25766  hvmul2negi  25965  hvadd12i  25974  hvnegdii  25979  normlem1  26027  normlem9  26035  normsubi  26058  normpar2i  26073  polid2i  26074  chjassi  26404  chj12i  26440  pjoml2i  26503  hoadd12i  26696  lnophmlem2  26936  nmopcoadj2i  27021  partfun  27516  ffsrn  27552  archirngz  27733  sqsscirc1  27890  sigaclfu2  28121  eulerpartlemd  28305  coinflippvt  28423  ballotth  28476  gam1  28607  quad3  29024  bpoly3  29820  onint1  29914  cnambfre  30063  dvcnsqrt  30101  rabren3dioph  30749  arearect  31183  areaquad  31184  lhe4.4ex1a  31234  expgrowthi  31238  expgrowth  31240  binomcxplemnotnn0  31261  dvcosre  31706  stoweidlem34  31816  fouriersw  32014  bj-csbsn  34471

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