Theorem sseldd 3194

Description: Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
sseld.1	|- ( ph -> A C_ B )
sseldd.2	|- ( ph -> C e. A )

Assertion

Ref	Expression
sseldd	|- ( ph -> C e. B )

Proof of Theorem sseldd

Step	Hyp	Ref	Expression
1		sseldd.2	. 2 |- ( ph -> C e. A )
2		sseld.1	. . 3 |- ( ph -> A C_ B )
3	2	sseld 3192	. 2 |- ( ph -> ( C e. A -> C e. B ) )
4	1, 3	mpd 13	1 |- ( ph -> C e. B )

Syntax hints:   -> wi 4   e. wcel 2176   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  disjiun  4039  exmid01  4242  frirrg  4397  ordtri2or2exmid  4619  ontri2orexmidim  4620  riotass  5927  tfrcldm  6449  nntr2  6589  eroveu  6713  eroprf  6715  ixpssmapg  6815  findcard2d  6988  findcard2sd  6989  fimax2gtrilemstep  6997  undifdc  7021  fisseneq  7031  fidcenumlemrks  7055  fidcenumlemr  7057  fiuni  7080  suplub2ti  7103  ctssdclemn0  7212  acfun  7319  ccfunen  7376  nnppipi  7456  archnqq  7530  prarloclemlt  7606  suplocexprlemrl  7830  suplocexprlemmu  7831  suplocexprlemdisj  7833  suplocexprlemloc  7834  suplocexprlemex  7835  suplocexprlemub  7836  suplocexprlemlub  7837  suplocsrlemb  7919  suplocsrlempr  7920  suplocsrlem  7921  axpre-suploclemres  8014  suprubex  9024  suprzclex  9471  infregelbex  9719  fzssp1  10189  elfzoelz  10269  fzofzp1  10356  fzostep1  10366  zssinfcl  10375  suprzubdc  10379  zsupssdc  10381  suprzcl2dc  10382  frecuzrdgg  10561  frecuzrdgdomlem  10562  frecuzrdgsuctlem  10568  ser3mono  10632  seqf1oglem2a  10663  seqf1oglem2  10665  bcm1k  10905  fimaxq  10972  leisorel  10982  zfz1isolemiso  10984  seq3coll  10987  fun2dmnop0  10992  swrdclg  11103  fimaxre2  11538  summodclem2a  11692  fsum3cvg3  11707  fsumcl2lem  11709  fsum0diaglem  11751  fsumiun  11788  prodmodclem2a  11887  fprodcl2lem  11916  fprodap0  11932  fprodrec  11940  fprodap0f  11947  fprodle  11951  bitsfzolem  12265  bitsfzo  12266  uzwodc  12358  4sqlemffi  12719  ennnfonelemhom  12786  exmidunben  12797  ctiunctlemfo  12810  nninfdclemcl  12819  nninfdclemp1  12821  nninfdclemlt  12822  nninfdclemf1  12823  unbendc  12825  strsetsid  12865  strslssd  12879  gsumpropd2  13225  gsumress  13227  resmhm  13319  mhmima  13323  grpidssd  13408  grpinvssd  13409  mulgnnsubcl  13470  mulgnn0subcl  13471  mulgsubcl  13472  mulgpropdg  13500  submmulg  13502  subg0  13516  subgsubcl  13521  subgsub  13522  subgmulg  13524  issubg4m  13529  nsgconj  13542  ssnmz  13547  ghmnsgima  13604  subgabl  13668  rdivmuldivd  13906  rhmunitinv  13940  subrguss  13998  subrginv  13999  subrgdv  14000  lsselg  14123  islss3  14141  lspsnel3  14167  lsspropdg  14193  rnglidlmcl  14242  znf1o  14413  topssnei  14634  cnprcl2k  14678  cnss1  14698  cnptopresti  14710  cnptoprest  14711  lmres  14720  txopn  14737  txcnp  14743  xmetres2  14851  blin2  14904  blopn  14962  xmettxlem  14981  xmettx  14982  elcncf2  15046  cncfmet  15064  cncfmptc  15068  cncfmptid  15069  negcncf  15077  mulcncflem  15079  cnrehmeocntop  15082  dedekindeulemuub  15089  dedekindeulemlu  15093  suplociccreex  15096  suplociccex  15097  dedekindicclemuub  15098  dedekindicclemlu  15102  dedekindicclemeu  15103  dedekindicclemicc  15104  ivthinclemlopn  15108  ivthinclemuopn  15110  ivthdec  15116  limcimolemlt  15136  cnplimcim  15139  cnplimclemle  15140  cnplimclemr  15141  cnlimci  15145  limccnpcntop  15147  limccnp2lem  15148  limccnp2cntop  15149  dvlemap  15152  dvfgg  15160  dvidsslem  15165  dvconstss  15170  dvcnp2cntop  15171  dvaddxxbr  15173  dvmulxxbr  15174  dvcoapbr  15179  dvcjbr  15180  plyf  15209  plycolemc  15230  dvply2g  15238  reeff1olem  15243  lgsquadlem3  15556  sssneq  15939