Theorem eqeltrdi 2325

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2205

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 2216

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

This theorem is referenced by:  eqeltrrdi  2326  snexprc  4301  onsucelsucexmidlem  4653  dcextest  4705  nnpredcl  4747  ovprc  6088  nnmcl  6716  xpsnen  7074  pw1fin  7172  xpfi  7194  mapfi  7216  snexxph  7222  0fsupp  7253  ctssdclemn0  7403  nninfisollemne  7424  nninfisol  7426  exmidonfinlem  7498  pw1on  7538  indpi  7659  nq0m0r  7773  genpelxp  7828  un0mulcl  9532  znegcl  9610  zeo  9686  eqreznegel  9949  xnegcl  10168  modqid0  10716  q2txmodxeq0  10750  ser0  10899  expcllem  10916  m1expcl2  10927  nn0ltexp2  11075  bcval  11115  bccl  11133  hashinfom  11145  lswex  11280  pfxclz  11375  pfxwrdsymbg  11386  cats1un  11417  cats1fvn  11460  cats1fvnd  11461  resqrexlemlo  11702  iserge0  12032  sumrbdclem  12067  fsum3cvg  12068  summodclem3  12070  summodclem2a  12071  fisumss  12082  binom  12174  bcxmas  12179  prodf1  12232  prodrbdclem  12261  fproddccvg  12262  prodmodclem2a  12266  fprodntrivap  12274  prodssdc  12279  fprodssdc  12280  gcdval  12659  gcdcl  12666  lcmcl  12773  pcxnn0cl  13012  pcxcl  13013  pcmptcl  13044  infpnlem2  13062  zgz  13075  4sqlem19  13111  znf1o  14816  ssblps  15307  ssbl  15308  xmeter  15318  blssioo  15435  elply  15616  plycj  15643  1sgmprm  15879  lgslem4  15893  lgsne0  15928  2sqlem9  16014  2sqlem10  16015  uhgr0enedgfi  16248  vtxdgfi0e  16307  eulerpathprum  16492  bj-charfun  16594  012of  16784  2o01f  16785  nninfsellemeqinf  16811  nninffeq  16815  trilpolemclim  16837  iswomni0  16853