Theorem eleqtrdi 2322

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
eleqtrdi.1	|- ( ph -> A e. B )
eleqtrdi.2	|- B = C

Assertion

Ref	Expression
eleqtrdi	|- ( ph -> A e. C )

Proof of Theorem eleqtrdi

Step	Hyp	Ref	Expression
1		eleqtrdi.1	. 2 |- ( ph -> A e. B )
2		eleqtrdi.2	. . 3 |- B = C
3	2	a1i 9	. 2 |- ( ph -> B = C )
4	1, 3	eleqtrd 2308	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:  eleqtrrdi  2323  prid2g  3771  freccllem  6548  nninfisol  7300  finomni  7307  exmidomniim  7308  ismkvnex  7322  exmidaclem  7390  pw1m  7409  caucvgprprlem2  7897  gt0srpr  7935  eluzel2  9727  fseq1p1m1  10290  fznn0sub2  10324  nn0split  10332  nnsplit  10333  exple1  10817  bcval5  10985  bcpasc  10988  zfz1isolemsplit  11060  seq3coll  11064  ccatrn  11144  swrdccat2  11203  cats1un  11253  pfxccatin12lem3  11264  cats1fvd  11298  clim2ser  11848  clim2ser2  11849  iserex  11850  isermulc2  11851  iserle  11853  iserge0  11854  climub  11855  climserle  11856  serf0  11863  summodclem3  11891  summodclem2a  11892  fsum3  11898  sum0  11899  fsumcl2lem  11909  fsumadd  11917  isumclim3  11934  isumadd  11942  fsump1i  11944  fsummulc2  11959  cvgcmpub  11987  binom1dif  11998  isumshft  12001  isumsplit  12002  isumrpcl  12005  arisum2  12010  trireciplem  12011  geoserap  12018  geolim  12022  geo2lim  12027  cvgratnnlemnexp  12035  cvgratnnlemseq  12037  cvgratgt0  12044  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  clim2prod  12050  clim2divap  12051  prodmodclem3  12086  prodmodclem2a  12087  fprodseq  12094  fprodntrivap  12095  fprodssdc  12101  fprodmul  12102  fprodabs  12127  fprodeq0  12128  efcvgfsum  12178  efcj  12184  effsumlt  12203  mod2eq1n2dvds  12390  bitsfzolem  12465  bitsfzo  12466  bitsfi  12468  bitsinv1lem  12472  bitsinv1  12473  nninfctlemfo  12561  algrp1  12568  phiprmpw  12744  crth  12746  phimullem  12747  prmdiv  12757  pcpremul  12816  pcmpt  12866  pcfac  12873  pockthlem  12879  pockthg  12880  1arith  12890  ennnfonelemp1  12977  nninfdclemp1  13021  relelbasov  13095  gsumwsubmcl  13529  gsumwmhm  13531  mulgnnp1  13667  mulgnn0z  13686  mulgnndir  13688  idomdomd  14241  idomcringd  14242  lspprid2  14376  istps  14706  topontopn  14711  cldrcl  14776  cnrehmeocntop  15284  elplyd  15415  ply1termlem  15416  ply1term  15417  plyaddlem1  15421  plymullem1  15422  plyaddlem  15423  plymullem  15424  plycoeid3  15431  plycolemc  15432  plycj  15435  dvply1  15439  0sgmppw  15667  1sgmprm  15668  lgsval2lem  15689  lgsdir2lem3  15709  lgsdir2lem5  15711  lgsdir  15714  lgsdilem2  15715  lgsdi  15716  lgsne0  15717  gausslemma2dlem3  15742  lgseisenlem1  15749  lgseisenlem4  15752  lgsquadlem2  15757  umgrpredgv  15945  2omap  16359  nnsf  16371  nninfsellemqall  16381  nninfomnilem  16384  nnnninfex  16388  nninfnfiinf  16389  cvgcmp2nlemabs  16400  trilpolemeq1  16408  nconstwlpolemgt0  16432