Theorem eqeltrdi 2256

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

Syntax hints:   -> wi 4   = wceq 1343   e. wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  eqeltrrdi  2257  snexprc  4164  onsucelsucexmidlem  4505  dcextest  4557  nnpredcl  4599  ovprc  5873  nnmcl  6445  xpsnen  6783  pw1fin  6872  xpfi  6891  snexxph  6911  ctssdclemn0  7071  nninfisollemne  7091  nninfisol  7093  exmidonfinlem  7145  pw1on  7178  indpi  7279  nq0m0r  7393  genpelxp  7448  un0mulcl  9144  znegcl  9218  zeo  9292  eqreznegel  9548  xnegcl  9764  modqid0  10281  q2txmodxeq0  10315  ser0  10445  expcllem  10462  m1expcl2  10473  nn0ltexp2  10619  bcval  10658  bccl  10676  hashinfom  10687  resqrexlemlo  10951  iserge0  11280  sumrbdclem  11314  fsum3cvg  11315  summodclem3  11317  summodclem2a  11318  fisumss  11329  binom  11421  bcxmas  11426  prodf1  11479  prodrbdclem  11508  fproddccvg  11509  prodmodclem2a  11513  fprodntrivap  11521  prodssdc  11526  fprodssdc  11527  gcdval  11888  gcdcl  11895  lcmcl  12000  pcxnn0cl  12238  pcxcl  12239  pcmptcl  12268  infpnlem2  12286  zgz  12299  ssblps  13025  ssbl  13026  xmeter  13036  blssioo  13145  lgslem4  13504  lgsne0  13539  2sqlem9  13560  2sqlem10  13561  bj-charfun  13649  012of  13835  2o01f  13836  nninfsellemeqinf  13856  nninffeq  13860  trilpolemclim  13875  iswomni0  13890