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 1398   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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  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  4282  onsucelsucexmidlem  4633  dcextest  4685  nnpredcl  4727  ovprc  6064  nnmcl  6692  xpsnen  7048  pw1fin  7145  xpfi  7167  snexxph  7192  0fsupp  7223  ctssdclemn0  7369  nninfisollemne  7390  nninfisol  7392  exmidonfinlem  7464  pw1on  7504  indpi  7622  nq0m0r  7736  genpelxp  7791  un0mulcl  9495  znegcl  9571  zeo  9646  eqreznegel  9909  xnegcl  10128  modqid0  10675  q2txmodxeq0  10709  ser0  10858  expcllem  10875  m1expcl2  10886  nn0ltexp2  11034  bcval  11074  bccl  11092  hashinfom  11103  lswex  11231  pfxclz  11326  pfxwrdsymbg  11337  cats1un  11368  cats1fvn  11411  cats1fvnd  11412  resqrexlemlo  11653  iserge0  11983  sumrbdclem  12018  fsum3cvg  12019  summodclem3  12021  summodclem2a  12022  fisumss  12033  binom  12125  bcxmas  12130  prodf1  12183  prodrbdclem  12212  fproddccvg  12213  prodmodclem2a  12217  fprodntrivap  12225  prodssdc  12230  fprodssdc  12231  gcdval  12610  gcdcl  12617  lcmcl  12724  pcxnn0cl  12963  pcxcl  12964  pcmptcl  12995  infpnlem2  13013  zgz  13026  4sqlem19  13062  znf1o  14747  ssblps  15236  ssbl  15237  xmeter  15247  blssioo  15364  elply  15545  plycj  15572  1sgmprm  15808  lgslem4  15822  lgsne0  15857  2sqlem9  15943  2sqlem10  15944  uhgr0enedgfi  16177  vtxdgfi0e  16236  eulerpathprum  16421  bj-charfun  16523  012of  16713  2o01f  16714  nninfsellemeqinf  16742  nninffeq  16746  trilpolemclim  16768  iswomni0  16784