Theorem eqeltrdi 2278

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

Syntax hints:   -> wi 4   = wceq 1363   e. wcel 2158

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-clel 2183

This theorem is referenced by:  eqeltrrdi  2279  snexprc  4198  onsucelsucexmidlem  4540  dcextest  4592  nnpredcl  4634  ovprc  5923  nnmcl  6496  xpsnen  6835  pw1fin  6924  xpfi  6943  snexxph  6963  ctssdclemn0  7123  nninfisollemne  7143  nninfisol  7145  exmidonfinlem  7206  pw1on  7239  indpi  7355  nq0m0r  7469  genpelxp  7524  un0mulcl  9224  znegcl  9298  zeo  9372  eqreznegel  9628  xnegcl  9846  modqid0  10364  q2txmodxeq0  10398  ser0  10528  expcllem  10545  m1expcl2  10556  nn0ltexp2  10703  bcval  10743  bccl  10761  hashinfom  10772  resqrexlemlo  11036  iserge0  11365  sumrbdclem  11399  fsum3cvg  11400  summodclem3  11402  summodclem2a  11403  fisumss  11414  binom  11506  bcxmas  11511  prodf1  11564  prodrbdclem  11593  fproddccvg  11594  prodmodclem2a  11598  fprodntrivap  11606  prodssdc  11611  fprodssdc  11612  gcdval  11974  gcdcl  11981  lcmcl  12086  pcxnn0cl  12324  pcxcl  12325  pcmptcl  12354  infpnlem2  12372  zgz  12385  ssblps  14221  ssbl  14222  xmeter  14232  blssioo  14341  lgslem4  14700  lgsne0  14735  2sqlem9  14767  2sqlem10  14768  bj-charfun  14855  012of  15042  2o01f  15043  nninfsellemeqinf  15062  nninffeq  15066  trilpolemclim  15081  iswomni0  15096