Theorem syl6eqel 2205

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
syl6eqel.1	|- ( ph -> A = B )
syl6eqel.2	|- B e. C

Assertion

Ref	Expression
syl6eqel	|- ( ph -> A e. C )

Proof of Theorem syl6eqel

Step	Hyp	Ref	Expression
1		syl6eqel.1	. 2 |- ( ph -> A = B )
2		syl6eqel.2	. . 3 |- B e. C
3	2	a1i 9	. 2 |- ( ph -> B e. C )
4	1, 3	eqeltrd 2191	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1314   e. wcel 1463

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111

This theorem is referenced by:  syl6eqelr  2206  snexprc  4070  onsucelsucexmidlem  4404  dcextest  4455  nnpredcl  4496  ovprc  5760  nnmcl  6331  xpsnen  6668  xpfi  6771  snexxph  6790  ctssdclemn0  6947  indpi  7098  nq0m0r  7212  genpelxp  7267  un0mulcl  8915  znegcl  8989  zeo  9060  eqreznegel  9308  xnegcl  9508  modqid0  10016  q2txmodxeq0  10050  ser0  10180  expcllem  10197  m1expcl2  10208  bcval  10388  bccl  10406  hashinfom  10417  resqrexlemlo  10677  iserge0  11004  sumrbdclem  11037  fsum3cvg  11038  summodclem3  11041  summodclem2a  11042  fisumss  11053  binom  11145  bcxmas  11150  gcdval  11496  gcdcl  11503  lcmcl  11599  ssblps  12414  ssbl  12415  xmeter  12425  blssioo  12531  nninfsellemeqinf  12904  nninffeq  12908  isomninnlem  12917  trilpolemclim  12921