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  6037  nnmcl  6627  xpsnen  6980  pw1fin  7072  xpfi  7094  snexxph  7117  ctssdclemn0  7277  nninfisollemne  7298  nninfisol  7300  exmidonfinlem  7371  pw1on  7411  indpi  7529  nq0m0r  7643  genpelxp  7698  un0mulcl  9403  znegcl  9477  zeo  9552  eqreznegel  9809  xnegcl  10028  modqid0  10572  q2txmodxeq0  10606  ser0  10755  expcllem  10772  m1expcl2  10783  nn0ltexp2  10931  bcval  10971  bccl  10989  hashinfom  11000  lswex  11123  pfxclz  11211  pfxwrdsymbg  11222  cats1un  11253  cats1fvn  11296  cats1fvnd  11297  resqrexlemlo  11524  iserge0  11854  sumrbdclem  11888  fsum3cvg  11889  summodclem3  11891  summodclem2a  11892  fisumss  11903  binom  11995  bcxmas  12000  prodf1  12053  prodrbdclem  12082  fproddccvg  12083  prodmodclem2a  12087  fprodntrivap  12095  prodssdc  12100  fprodssdc  12101  gcdval  12480  gcdcl  12487  lcmcl  12594  pcxnn0cl  12833  pcxcl  12834  pcmptcl  12865  infpnlem2  12883  zgz  12896  4sqlem19  12932  znf1o  14615  ssblps  15099  ssbl  15100  xmeter  15110  blssioo  15227  elply  15408  plycj  15435  1sgmprm  15668  lgslem4  15682  lgsne0  15717  2sqlem9  15803  2sqlem10  15804  bj-charfun  16170  012of  16357  2o01f  16358  nninfsellemeqinf  16382  nninffeq  16386  trilpolemclim  16404  iswomni0  16419