Theorem sseldd 3225

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

Syntax hints:   -> wi 4   e. wcel 2200   C_ wss 3197

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-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  disjiun  4078  exmid01  4282  frirrg  4441  ordtri2or2exmid  4663  ontri2orexmidim  4664  riotass  5990  elovimad  6051  tfrcldm  6515  nntr2  6657  eroveu  6781  eroprf  6783  ixpssmapg  6883  findcard2d  7061  findcard2sd  7062  fimax2gtrilemstep  7071  elssdc  7075  eqsndc  7076  undifdc  7097  fisseneq  7107  fidcenumlemrks  7131  fidcenumlemr  7133  fiuni  7156  suplub2ti  7179  ctssdclemn0  7288  acfun  7400  ccfunen  7461  nnppipi  7541  archnqq  7615  prarloclemlt  7691  suplocexprlemrl  7915  suplocexprlemmu  7916  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemex  7920  suplocexprlemub  7921  suplocexprlemlub  7922  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  axpre-suploclemres  8099  suprubex  9109  suprzclex  9556  infregelbex  9805  fzssp1  10275  elfzoelz  10355  fzofzp1  10445  fzostep1  10455  zssinfcl  10464  suprzubdc  10468  zsupssdc  10470  suprzcl2dc  10471  frecuzrdgg  10650  frecuzrdgdomlem  10651  frecuzrdgsuctlem  10657  ser3mono  10721  seqf1oglem2a  10752  seqf1oglem2  10754  bcm1k  10994  fimaxq  11062  leisorel  11072  zfz1isolemiso  11074  seq3coll  11077  fun2dmnop0  11082  swrdclg  11197  fimaxre2  11753  summodclem2a  11907  fsum3cvg3  11922  fsumcl2lem  11924  fsum0diaglem  11966  fsumiun  12003  prodmodclem2a  12102  fprodcl2lem  12131  fprodap0  12147  fprodrec  12155  fprodap0f  12162  fprodle  12166  bitsfzolem  12480  bitsfzo  12481  uzwodc  12573  4sqlemffi  12934  ennnfonelemhom  13001  exmidunben  13012  ctiunctlemfo  13025  nninfdclemcl  13034  nninfdclemp1  13036  nninfdclemlt  13037  nninfdclemf1  13038  unbendc  13040  strsetsid  13080  strslssd  13094  gsumpropd2  13441  gsumress  13443  resmhm  13535  mhmima  13539  grpidssd  13624  grpinvssd  13625  mulgnnsubcl  13686  mulgnn0subcl  13687  mulgsubcl  13688  mulgpropdg  13716  submmulg  13718  subg0  13732  subgsubcl  13737  subgsub  13738  subgmulg  13740  issubg4m  13745  nsgconj  13758  ssnmz  13763  ghmnsgima  13820  subgabl  13884  rdivmuldivd  14123  rhmunitinv  14157  subrguss  14215  subrginv  14216  subrgdv  14217  lsselg  14340  islss3  14358  lspsnel3  14384  lsspropdg  14410  rnglidlmcl  14459  znf1o  14630  topssnei  14851  cnprcl2k  14895  cnss1  14915  cnptopresti  14927  cnptoprest  14928  lmres  14937  txopn  14954  txcnp  14960  xmetres2  15068  blin2  15121  blopn  15179  xmettxlem  15198  xmettx  15199  elcncf2  15263  cncfmet  15281  cncfmptc  15285  cncfmptid  15286  negcncf  15294  mulcncflem  15296  cnrehmeocntop  15299  dedekindeulemuub  15306  dedekindeulemlu  15310  suplociccreex  15313  suplociccex  15314  dedekindicclemuub  15315  dedekindicclemlu  15319  dedekindicclemeu  15320  dedekindicclemicc  15321  ivthinclemlopn  15325  ivthinclemuopn  15327  ivthdec  15333  limcimolemlt  15353  cnplimcim  15356  cnplimclemle  15357  cnplimclemr  15358  cnlimci  15362  limccnpcntop  15364  limccnp2lem  15365  limccnp2cntop  15366  dvlemap  15369  dvfgg  15377  dvidsslem  15382  dvconstss  15387  dvcnp2cntop  15388  dvaddxxbr  15390  dvmulxxbr  15391  dvcoapbr  15396  dvcjbr  15397  plyf  15426  plycolemc  15447  dvply2g  15455  reeff1olem  15460  lgsquadlem3  15773  upgrex  15918  wlkvtxiedg  16086  wlkvtxiedgg  16087  sssneq  16427