Theorem sseldd 3180

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

Syntax hints:   -> wi 4   e. wcel 2164   C_ wss 3153

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  disjiun  4024  exmid01  4227  frirrg  4381  ordtri2or2exmid  4603  ontri2orexmidim  4604  riotass  5901  tfrcldm  6416  nntr2  6556  eroveu  6680  eroprf  6682  ixpssmapg  6782  findcard2d  6947  findcard2sd  6948  fimax2gtrilemstep  6956  undifdc  6980  fisseneq  6988  fidcenumlemrks  7012  fidcenumlemr  7014  fiuni  7037  suplub2ti  7060  ctssdclemn0  7169  acfun  7267  ccfunen  7324  nnppipi  7403  archnqq  7477  prarloclemlt  7553  suplocexprlemrl  7777  suplocexprlemmu  7778  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemex  7782  suplocexprlemub  7783  suplocexprlemlub  7784  suplocsrlemb  7866  suplocsrlempr  7867  suplocsrlem  7868  axpre-suploclemres  7961  suprubex  8970  suprzclex  9415  infregelbex  9663  fzssp1  10133  elfzoelz  10213  fzofzp1  10294  fzostep1  10304  frecuzrdgg  10487  frecuzrdgdomlem  10488  frecuzrdgsuctlem  10494  ser3mono  10558  seqf1oglem2a  10589  seqf1oglem2  10591  bcm1k  10831  fimaxq  10898  leisorel  10908  zfz1isolemiso  10910  seq3coll  10913  fimaxre2  11370  summodclem2a  11524  fsum3cvg3  11539  fsumcl2lem  11541  fsum0diaglem  11583  fsumiun  11620  prodmodclem2a  11719  fprodcl2lem  11748  fprodap0  11764  fprodrec  11772  fprodap0f  11779  fprodle  11783  zssinfcl  12085  suprzubdc  12089  zsupssdc  12091  suprzcl2dc  12092  uzwodc  12174  4sqlemffi  12534  ennnfonelemhom  12572  exmidunben  12583  ctiunctlemfo  12596  nninfdclemcl  12605  nninfdclemp1  12607  nninfdclemlt  12608  nninfdclemf1  12609  unbendc  12611  strsetsid  12651  strslssd  12665  gsumpropd2  12976  gsumress  12978  resmhm  13059  mhmima  13063  grpidssd  13148  grpinvssd  13149  mulgnnsubcl  13204  mulgnn0subcl  13205  mulgsubcl  13206  mulgpropdg  13234  submmulg  13236  subg0  13250  subgsubcl  13255  subgsub  13256  subgmulg  13258  issubg4m  13263  nsgconj  13276  ssnmz  13281  ghmnsgima  13338  subgabl  13402  rdivmuldivd  13640  rhmunitinv  13674  subrguss  13732  subrginv  13733  subrgdv  13734  lsselg  13857  islss3  13875  lspsnel3  13901  lsspropdg  13927  rnglidlmcl  13976  znf1o  14139  topssnei  14330  cnprcl2k  14374  cnss1  14394  cnptopresti  14406  cnptoprest  14407  lmres  14416  txopn  14433  txcnp  14439  xmetres2  14547  blin2  14600  blopn  14658  xmettxlem  14677  xmettx  14678  elcncf2  14729  cncfmet  14747  cncfmptc  14750  cncfmptid  14751  negcncf  14759  mulcncflem  14761  cnrehmeocntop  14764  dedekindeulemuub  14771  dedekindeulemlu  14775  suplociccreex  14778  suplociccex  14779  dedekindicclemuub  14780  dedekindicclemlu  14784  dedekindicclemeu  14785  dedekindicclemicc  14786  ivthinclemlopn  14790  ivthinclemuopn  14792  ivthdec  14798  limcimolemlt  14818  cnplimcim  14821  cnplimclemle  14822  cnplimclemr  14823  cnlimci  14827  limccnpcntop  14829  limccnp2lem  14830  limccnp2cntop  14831  dvlemap  14834  dvfgg  14842  dvcnp2cntop  14848  dvaddxxbr  14850  dvmulxxbr  14851  dvcoapbr  14856  dvcjbr  14857  plyf  14883  reeff1olem  14906  sssneq  15492