Theorem sseldd 3202

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 3200	. 2 |- ( ph -> ( C e. A -> C e. B ) )
4	1, 3	mpd 13	1 |- ( ph -> C e. B )

Syntax hints:   -> wi 4   e. wcel 2178   C_ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  disjiun  4054  exmid01  4258  frirrg  4415  ordtri2or2exmid  4637  ontri2orexmidim  4638  riotass  5950  tfrcldm  6472  nntr2  6612  eroveu  6736  eroprf  6738  ixpssmapg  6838  findcard2d  7014  findcard2sd  7015  fimax2gtrilemstep  7023  undifdc  7047  fisseneq  7057  fidcenumlemrks  7081  fidcenumlemr  7083  fiuni  7106  suplub2ti  7129  ctssdclemn0  7238  acfun  7350  ccfunen  7411  nnppipi  7491  archnqq  7565  prarloclemlt  7641  suplocexprlemrl  7865  suplocexprlemmu  7866  suplocexprlemdisj  7868  suplocexprlemloc  7869  suplocexprlemex  7870  suplocexprlemub  7871  suplocexprlemlub  7872  suplocsrlemb  7954  suplocsrlempr  7955  suplocsrlem  7956  axpre-suploclemres  8049  suprubex  9059  suprzclex  9506  infregelbex  9754  fzssp1  10224  elfzoelz  10304  fzofzp1  10393  fzostep1  10403  zssinfcl  10412  suprzubdc  10416  zsupssdc  10418  suprzcl2dc  10419  frecuzrdgg  10598  frecuzrdgdomlem  10599  frecuzrdgsuctlem  10605  ser3mono  10669  seqf1oglem2a  10700  seqf1oglem2  10702  bcm1k  10942  fimaxq  11009  leisorel  11019  zfz1isolemiso  11021  seq3coll  11024  fun2dmnop0  11029  swrdclg  11141  fimaxre2  11653  summodclem2a  11807  fsum3cvg3  11822  fsumcl2lem  11824  fsum0diaglem  11866  fsumiun  11903  prodmodclem2a  12002  fprodcl2lem  12031  fprodap0  12047  fprodrec  12055  fprodap0f  12062  fprodle  12066  bitsfzolem  12380  bitsfzo  12381  uzwodc  12473  4sqlemffi  12834  ennnfonelemhom  12901  exmidunben  12912  ctiunctlemfo  12925  nninfdclemcl  12934  nninfdclemp1  12936  nninfdclemlt  12937  nninfdclemf1  12938  unbendc  12940  strsetsid  12980  strslssd  12994  gsumpropd2  13340  gsumress  13342  resmhm  13434  mhmima  13438  grpidssd  13523  grpinvssd  13524  mulgnnsubcl  13585  mulgnn0subcl  13586  mulgsubcl  13587  mulgpropdg  13615  submmulg  13617  subg0  13631  subgsubcl  13636  subgsub  13637  subgmulg  13639  issubg4m  13644  nsgconj  13657  ssnmz  13662  ghmnsgima  13719  subgabl  13783  rdivmuldivd  14021  rhmunitinv  14055  subrguss  14113  subrginv  14114  subrgdv  14115  lsselg  14238  islss3  14256  lspsnel3  14282  lsspropdg  14308  rnglidlmcl  14357  znf1o  14528  topssnei  14749  cnprcl2k  14793  cnss1  14813  cnptopresti  14825  cnptoprest  14826  lmres  14835  txopn  14852  txcnp  14858  xmetres2  14966  blin2  15019  blopn  15077  xmettxlem  15096  xmettx  15097  elcncf2  15161  cncfmet  15179  cncfmptc  15183  cncfmptid  15184  negcncf  15192  mulcncflem  15194  cnrehmeocntop  15197  dedekindeulemuub  15204  dedekindeulemlu  15208  suplociccreex  15211  suplociccex  15212  dedekindicclemuub  15213  dedekindicclemlu  15217  dedekindicclemeu  15218  dedekindicclemicc  15219  ivthinclemlopn  15223  ivthinclemuopn  15225  ivthdec  15231  limcimolemlt  15251  cnplimcim  15254  cnplimclemle  15255  cnplimclemr  15256  cnlimci  15260  limccnpcntop  15262  limccnp2lem  15263  limccnp2cntop  15264  dvlemap  15267  dvfgg  15275  dvidsslem  15280  dvconstss  15285  dvcnp2cntop  15286  dvaddxxbr  15288  dvmulxxbr  15289  dvcoapbr  15294  dvcjbr  15295  plyf  15324  plycolemc  15345  dvply2g  15353  reeff1olem  15358  lgsquadlem3  15671  upgrex  15814  sssneq  16141