MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sstrd Structured version   Unicode version

Theorem sstrd 3350
Description: Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)
Hypotheses
Ref Expression
sstrd.1  |-  ( ph  ->  A  C_  B )
sstrd.2  |-  ( ph  ->  B  C_  C )
Assertion
Ref Expression
sstrd  |-  ( ph  ->  A  C_  C )

Proof of Theorem sstrd
StepHypRef Expression
1 sstrd.1 . 2  |-  ( ph  ->  A  C_  B )
2 sstrd.2 . 2  |-  ( ph  ->  B  C_  C )
3 sstr 3348 . 2  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3312
This theorem is referenced by:  syl5ss  3351  syl6ss  3352  ssdif2d  3478  uniintsn  4079  tfisi  4830  funss  5464  fssxp  5594  knatar  6072  suppssfv  6293  suppssov1  6294  tposss  6472  omwordri  6807  oewordri  6827  oeeui  6837  oaabs2  6880  omopthlem1  6890  ecinxp  6971  sbthlem1  7209  dffi2  7420  hartogslem1  7503  cantnfcl  7614  cantnflt  7619  cantnfp1lem3  7628  cantnflem3  7639  cnfcom  7649  cnfcom3lem  7652  rankssb  7766  tskwe  7829  dfac12lem2  8016  dfac12lem3  8017  cfflb  8131  cfcof  8146  ssfin2  8192  hsmexlem4  8301  ttukeylem6  8386  ttukeylem7  8387  fpwwe2lem1  8498  fpwwe2lem8  8504  fpwwe2lem11  8507  fpwwe2lem12  8508  canthnumlem  8515  canthwelem  8517  canthwe  8518  canthp1lem2  8520  pwfseqlem5  8530  wunex2  8605  tsktrss  8628  inttsk  8641  uzwo3  10561  seqsplit  11348  seqf1olem2a  11353  seqz  11363  swrdval2  11759  sumss  12510  qshash  12598  incexc  12609  incexc2  12610  rpnnen2lem11  12816  vdwlem1  13341  ramub1lem1  13386  imasaddvallem  13746  imasvscaf  13756  mrerintcl  13814  ismred2  13820  mremre  13821  mrcuni  13838  mressmrcd  13844  submrc  13845  mrissmrid  13858  mreexexlem2d  13862  isacs2  13870  isacs1i  13874  invss  13978  ssctr  14017  funcres2b  14086  isacs3lem  14584  acsfiindd  14595  acsmapd  14596  acsmap2d  14597  tsrdir  14675  subsubm  14749  gsumwspan  14783  subsubg  14955  subgint  14956  cntzidss  15128  pgpssslw  15240  lsmless1x  15270  lsmless2x  15271  lsmless12  15287  subglsm  15297  gsumval3  15506  gsumzadd  15519  gsum2d  15538  dmdprdd  15552  dprdfeq0  15572  dprdspan  15577  dprdres  15578  dprdss  15579  dprdz  15580  subgdmdprd  15584  subgdprd  15585  dprdsn  15586  dprd2dlem1  15591  dprd2da  15592  dmdprdsplit2lem  15595  dprdsplit  15598  pgpfac1lem2  15625  pgpfac1lem3  15627  pgpfac1lem5  15629  subsubrg  15886  lspss  16052  lspun  16055  lsslsp  16083  lmhmlsp  16117  lsmelval2  16149  lsmssspx  16152  lsppratlem2  16212  lsppratlem3  16213  lsppratlem4  16214  lbsextlem2  16223  lbsextlem3  16224  aspss  16383  ocvlsp  16895  cssmre  16912  obselocv  16947  obslbs  16949  toponmre  17149  neiint  17160  neiss  17165  lpss  17198  lpss3  17200  restopnb  17231  restfpw  17235  neitr  17236  restcls  17237  restntr  17238  restlp  17239  ordtbas  17248  pnfnei  17276  mnfnei  17277  iscnp4  17319  cnclsi  17328  isreg2  17433  discmp  17453  cmpcld  17457  uncmp  17458  sscmp  17460  hauscmplem  17461  cmpfi  17463  iunconlem  17482  clscon  17485  2ndcctbss  17510  restnlly  17537  llyrest  17540  nllyrest  17541  llyidm  17543  nllyidm  17544  cldllycmp  17550  dislly  17552  llycmpkgen2  17574  ptbasfi  17605  txnlly  17661  txcmplem1  17665  tx1stc  17674  xkococnlem  17683  qtopval2  17720  basqtop  17735  tgqtop  17736  qtoprest  17741  kqreglem1  17765  kqreglem2  17766  kqnrmlem1  17767  kqnrmlem2  17768  fsubbas  17891  fgabs  17903  fbasrn  17908  trfil2  17911  trfg  17915  isufil2  17932  trufil  17934  ssufl  17942  ufileu  17943  filufint  17944  fmfnfmlem4  17981  fmfnfm  17982  flimss2  17996  flimss1  17997  fclsfnflim  18051  flimfnfcls  18052  fclscmp  18054  cnpfcfi  18064  alexsubALT  18074  clssubg  18130  clsnsg  18131  ustexsym  18237  ustex2sym  18238  ustex3sym  18239  ustund  18243  ustneism  18245  trust  18251  utoptop  18256  restutopopn  18260  utop2nei  18272  utopreg  18274  cfiluweak  18317  neipcfilu  18318  blssps  18446  blss  18447  blcld  18527  blsscls  18529  met1stc  18543  met2ndci  18544  metustOLD  18589  metust  18590  cfilucfilOLD  18591  cfilucfil  18592  restmetu  18609  tgqioo  18823  xrsblre  18834  reconnlem2  18850  xrge0gsumle  18856  xrge0tsms  18857  rescncf  18919  cnmpt2pc  18945  cnheibor  18972  cnllycmp  18973  lebnum  18981  phtpycn  19000  cfilfcls  19219  iscmet3lem2  19237  cmetss  19259  cncmet  19267  bcthlem4  19272  bcth3  19276  minveclem4a  19323  minveclem4  19325  ivthicc  19347  ovollb  19367  ovollb2lem  19376  ovollb2  19377  nulmbl2  19423  ioorcl2  19456  uniioombllem3  19469  uniioombllem4  19470  uniioombllem5  19471  opnmbllem  19485  volcn  19490  volivth  19491  mbfeqalem  19526  itg10a  19594  mbfi1fseqlem4  19602  ditgcl  19737  ditgswap  19738  ditgsplitlem  19739  limcflf  19760  limcres  19765  dvbss  19780  dvbsss  19781  perfdvf  19782  dvreslem  19788  dvres2lem  19789  dvres3  19792  dvcnp  19797  dvcnp2  19798  dvcn  19799  dvnff  19801  dvn2bss  19808  dvnres  19809  cpnord  19813  dvaddbr  19816  dvmulbr  19817  dvcobr  19824  dvnfre  19830  dvmptres2  19840  dvmptntr  19849  dvcnvlem  19852  dvcnv  19853  dvferm1lem  19860  dvferm2lem  19862  dvlip  19869  dvlipcn  19870  dvlip2  19871  c1liplem1  19872  dvgt0lem1  19878  lhop1lem  19889  lhop  19892  dvcnvrelem1  19893  dvcnvrelem2  19894  dvcnvre  19895  dvfsumle  19897  dvfsumge  19898  dvfsumabs  19899  ftc1lem1  19911  ftc1lem2  19912  ftc1a  19913  ftc1lem4  19915  ftc2ditglem  19921  itgsubstlem  19924  ig1peu  20086  ig1pdvds  20091  taylfvallem1  20265  tayl0  20270  taylply2  20276  taylply  20277  dvtaylp  20278  dvntaylp  20279  dvntaylp0  20280  taylthlem1  20281  ulmdvlem1  20308  ulmdvlem3  20310  psercn  20334  pserdvlem2  20336  abelth  20349  xrlimcnp  20799  wilthlem2  20844  sqff1o  20957  chtublem  20987  pntlemq  21287  pntlemf  21291  ghsubgolem  21950  shintcli  22823  shub1  22876  mdslmd1lem1  23820  mdexchi  23830  chirredlem1  23885  mdsymlem5  23902  sumdmdii  23910  sumdmdlem2  23914  xrsupssd  24117  xrge0tsmsd  24215  pnfneige0  24328  insiga  24512  sssigagen2  24521  dya2iocnei  24624  sibfof  24646  lgamucov  24814  erdszelem7  24875  erdszelem8  24876  erdsze2lem1  24881  conpcon  24914  cvmliftmolem1  24960  cvmlift2lem1  24981  cvmlift2lem9  24990  cvmlift2lem10  24991  cvmlift3lem6  25003  cvmlift3lem7  25004  rtrclreclem.min  25139  prodss  25265  dftrpred3g  25503  nofulllem3  25651  ontgval  26173  mblfinlem  26234  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  comppfsc  26378  neibastop2lem  26380  fnemeet2  26387  fnejoin1  26388  sstotbnd2  26474  heiborlem1  26511  heiborlem8  26518  intidl  26630  elrfi  26739  ismrcd1  26743  istopclsd  26745  mrefg2  26752  aomclem2  27121  aomclem6  27125  hbtlem6  27301  hbt  27302  symggen  27379  stoweidlem59  27775  bnj906  29238  bnj1020  29271  bnj1137  29301  bnj1408  29342  bnj1452  29358  lsmsat  29743  lssats  29747  lpssat  29748  lssatle  29750  lssat  29751  lsatcvatlem  29784  paddss12  30553  paddasslem17  30570  pmodlem1  30580  pmod1i  30582  pmodl42N  30585  elpcliN  30627  pclfinN  30634  polcon3N  30651  polcon2N  30653  paddunN  30661  pclfinclN  30684  poml5N  30688  osumcllem1N  30690  osumcllem2N  30691  osumcllem3N  30692  pl42lem2N  30714  pl42lem4N  30716  cdlemn5pre  31935  dihord1  31953  dihord2a  31954  dihord2b  31955  dihord5b  31994  dochss  32100  dochdmj1  32125  djhsumss  32142  djhunssN  32144  dochexmidlem2  32196  lclkrslem1  32272  lclkrslem2  32273  lcfrlem2  32278
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator