Theorem eqeltrdi 2322

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

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eqeltrrdi  2323  snexprc  4276  onsucelsucexmidlem  4627  dcextest  4679  nnpredcl  4721  ovprc  6054  nnmcl  6649  xpsnen  7005  pw1fin  7102  xpfi  7124  snexxph  7149  ctssdclemn0  7309  nninfisollemne  7330  nninfisol  7332  exmidonfinlem  7404  pw1on  7444  indpi  7562  nq0m0r  7676  genpelxp  7731  un0mulcl  9436  znegcl  9510  zeo  9585  eqreznegel  9848  xnegcl  10067  modqid0  10613  q2txmodxeq0  10647  ser0  10796  expcllem  10813  m1expcl2  10824  nn0ltexp2  10972  bcval  11012  bccl  11030  hashinfom  11041  lswex  11169  pfxclz  11264  pfxwrdsymbg  11275  cats1un  11306  cats1fvn  11349  cats1fvnd  11350  resqrexlemlo  11591  iserge0  11921  sumrbdclem  11956  fsum3cvg  11957  summodclem3  11959  summodclem2a  11960  fisumss  11971  binom  12063  bcxmas  12068  prodf1  12121  prodrbdclem  12150  fproddccvg  12151  prodmodclem2a  12155  fprodntrivap  12163  prodssdc  12168  fprodssdc  12169  gcdval  12548  gcdcl  12555  lcmcl  12662  pcxnn0cl  12901  pcxcl  12902  pcmptcl  12933  infpnlem2  12951  zgz  12964  4sqlem19  13000  znf1o  14684  ssblps  15168  ssbl  15169  xmeter  15179  blssioo  15296  elply  15477  plycj  15504  1sgmprm  15737  lgslem4  15751  lgsne0  15786  2sqlem9  15872  2sqlem10  15873  uhgr0enedgfi  16106  vtxdgfi0e  16165  eulerpathprum  16350  bj-charfun  16453  012of  16643  2o01f  16644  nninfsellemeqinf  16669  nninffeq  16673  trilpolemclim  16691  iswomni0  16707