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  4230  onsucelsucexmidlem  4577  dcextest  4629  nnpredcl  4671  ovprc  5980  nnmcl  6567  xpsnen  6916  pw1fin  7007  xpfi  7029  snexxph  7052  ctssdclemn0  7212  nninfisollemne  7233  nninfisol  7235  exmidonfinlem  7301  pw1on  7338  indpi  7455  nq0m0r  7569  genpelxp  7624  un0mulcl  9329  znegcl  9403  zeo  9478  eqreznegel  9735  xnegcl  9954  modqid0  10495  q2txmodxeq0  10529  ser0  10678  expcllem  10695  m1expcl2  10706  nn0ltexp2  10854  bcval  10894  bccl  10912  hashinfom  10923  resqrexlemlo  11324  iserge0  11654  sumrbdclem  11688  fsum3cvg  11689  summodclem3  11691  summodclem2a  11692  fisumss  11703  binom  11795  bcxmas  11800  prodf1  11853  prodrbdclem  11882  fproddccvg  11883  prodmodclem2a  11887  fprodntrivap  11895  prodssdc  11900  fprodssdc  11901  gcdval  12280  gcdcl  12287  lcmcl  12394  pcxnn0cl  12633  pcxcl  12634  pcmptcl  12665  infpnlem2  12683  zgz  12696  4sqlem19  12732  znf1o  14413  ssblps  14897  ssbl  14898  xmeter  14908  blssioo  15025  elply  15206  plycj  15233  1sgmprm  15466  lgslem4  15480  lgsne0  15515  2sqlem9  15601  2sqlem10  15602  bj-charfun  15743  012of  15930  2o01f  15931  nninfsellemeqinf  15953  nninffeq  15957  trilpolemclim  15975  iswomni0  15990