Theorem eqeltrdi 2296

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

Hypotheses

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

Assertion

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

Proof of Theorem eqeltrdi

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

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eqeltrrdi  2297  snexprc  4231  onsucelsucexmidlem  4578  dcextest  4630  nnpredcl  4672  ovprc  5982  nnmcl  6569  xpsnen  6918  pw1fin  7009  xpfi  7031  snexxph  7054  ctssdclemn0  7214  nninfisollemne  7235  nninfisol  7237  exmidonfinlem  7303  pw1on  7340  indpi  7457  nq0m0r  7571  genpelxp  7626  un0mulcl  9331  znegcl  9405  zeo  9480  eqreznegel  9737  xnegcl  9956  modqid0  10497  q2txmodxeq0  10531  ser0  10680  expcllem  10697  m1expcl2  10708  nn0ltexp2  10856  bcval  10896  bccl  10914  hashinfom  10925  lswex  11047  pfxwrdsymbg  11144  resqrexlemlo  11357  iserge0  11687  sumrbdclem  11721  fsum3cvg  11722  summodclem3  11724  summodclem2a  11725  fisumss  11736  binom  11828  bcxmas  11833  prodf1  11886  prodrbdclem  11915  fproddccvg  11916  prodmodclem2a  11920  fprodntrivap  11928  prodssdc  11933  fprodssdc  11934  gcdval  12313  gcdcl  12320  lcmcl  12427  pcxnn0cl  12666  pcxcl  12667  pcmptcl  12698  infpnlem2  12716  zgz  12729  4sqlem19  12765  znf1o  14446  ssblps  14930  ssbl  14931  xmeter  14941  blssioo  15058  elply  15239  plycj  15266  1sgmprm  15499  lgslem4  15513  lgsne0  15548  2sqlem9  15634  2sqlem10  15635  bj-charfun  15780  012of  15967  2o01f  15968  nninfsellemeqinf  15990  nninffeq  15994  trilpolemclim  16012  iswomni0  16027