Theorem eqeltrdi 2298

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  eqeltrrdi  2299  snexprc  4246  onsucelsucexmidlem  4595  dcextest  4647  nnpredcl  4689  ovprc  6003  nnmcl  6590  xpsnen  6941  pw1fin  7033  xpfi  7055  snexxph  7078  ctssdclemn0  7238  nninfisollemne  7259  nninfisol  7261  exmidonfinlem  7332  pw1on  7372  indpi  7490  nq0m0r  7604  genpelxp  7659  un0mulcl  9364  znegcl  9438  zeo  9513  eqreznegel  9770  xnegcl  9989  modqid0  10532  q2txmodxeq0  10566  ser0  10715  expcllem  10732  m1expcl2  10743  nn0ltexp2  10891  bcval  10931  bccl  10949  hashinfom  10960  lswex  11082  pfxclz  11170  pfxwrdsymbg  11181  cats1un  11212  resqrexlemlo  11439  iserge0  11769  sumrbdclem  11803  fsum3cvg  11804  summodclem3  11806  summodclem2a  11807  fisumss  11818  binom  11910  bcxmas  11915  prodf1  11968  prodrbdclem  11997  fproddccvg  11998  prodmodclem2a  12002  fprodntrivap  12010  prodssdc  12015  fprodssdc  12016  gcdval  12395  gcdcl  12402  lcmcl  12509  pcxnn0cl  12748  pcxcl  12749  pcmptcl  12780  infpnlem2  12798  zgz  12811  4sqlem19  12847  znf1o  14528  ssblps  15012  ssbl  15013  xmeter  15023  blssioo  15140  elply  15321  plycj  15348  1sgmprm  15581  lgslem4  15595  lgsne0  15630  2sqlem9  15716  2sqlem10  15717  bj-charfun  15942  012of  16130  2o01f  16131  nninfsellemeqinf  16155  nninffeq  16159  trilpolemclim  16177  iswomni0  16192