Theorem eqeltrdi 2320

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 2306	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eqeltrrdi  2321  snexprc  4270  onsucelsucexmidlem  4621  dcextest  4673  nnpredcl  4715  ovprc  6043  nnmcl  6635  xpsnen  6988  pw1fin  7083  xpfi  7105  snexxph  7128  ctssdclemn0  7288  nninfisollemne  7309  nninfisol  7311  exmidonfinlem  7382  pw1on  7422  indpi  7540  nq0m0r  7654  genpelxp  7709  un0mulcl  9414  znegcl  9488  zeo  9563  eqreznegel  9821  xnegcl  10040  modqid0  10584  q2txmodxeq0  10618  ser0  10767  expcllem  10784  m1expcl2  10795  nn0ltexp2  10943  bcval  10983  bccl  11001  hashinfom  11012  lswex  11136  pfxclz  11227  pfxwrdsymbg  11238  cats1un  11269  cats1fvn  11312  cats1fvnd  11313  resqrexlemlo  11540  iserge0  11870  sumrbdclem  11904  fsum3cvg  11905  summodclem3  11907  summodclem2a  11908  fisumss  11919  binom  12011  bcxmas  12016  prodf1  12069  prodrbdclem  12098  fproddccvg  12099  prodmodclem2a  12103  fprodntrivap  12111  prodssdc  12116  fprodssdc  12117  gcdval  12496  gcdcl  12503  lcmcl  12610  pcxnn0cl  12849  pcxcl  12850  pcmptcl  12881  infpnlem2  12899  zgz  12912  4sqlem19  12948  znf1o  14631  ssblps  15115  ssbl  15116  xmeter  15126  blssioo  15243  elply  15424  plycj  15451  1sgmprm  15684  lgslem4  15698  lgsne0  15733  2sqlem9  15819  2sqlem10  15820  vtxdgfi0e  16055  bj-charfun  16253  012of  16444  2o01f  16445  nninfsellemeqinf  16470  nninffeq  16474  trilpolemclim  16492  iswomni0  16507