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

Theorem sstrd 3275
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 3273 . 2  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3238
This theorem is referenced by:  syl5ss  3276  syl6ss  3277  ssdif2d  3402  uniintsn  4001  tfisi  4752  funss  5376  fssxp  5506  knatar  5980  suppssfv  6201  suppssov1  6202  tposss  6377  omwordri  6712  oewordri  6732  oeeui  6742  oaabs2  6785  omopthlem1  6795  ecinxp  6876  sbthlem1  7114  dffi2  7323  hartogslem1  7404  cantnfcl  7515  cantnflt  7520  cantnfp1lem3  7529  cantnflem3  7540  cnfcom  7550  cnfcom3lem  7553  rankssb  7667  tskwe  7730  dfac12lem2  7917  dfac12lem3  7918  cfflb  8032  cfcof  8047  ssfin2  8093  hsmexlem4  8202  ttukeylem6  8288  ttukeylem7  8289  fpwwe2lem1  8400  fpwwe2lem8  8406  fpwwe2lem11  8409  fpwwe2lem12  8410  canthnumlem  8417  canthwelem  8419  canthwe  8420  canthp1lem2  8422  pwfseqlem5  8432  wunex2  8507  tsktrss  8530  inttsk  8543  uzwo3  10462  seqsplit  11243  seqf1olem2a  11248  seqz  11258  swrdval2  11654  sumss  12405  qshash  12493  incexc  12504  incexc2  12505  rpnnen2lem11  12711  vdwlem1  13236  ramub1lem1  13281  imasaddvallem  13641  imasvscaf  13651  mrerintcl  13709  ismred2  13715  mremre  13716  mrcuni  13733  mressmrcd  13739  submrc  13740  mrissmrid  13753  mreexexlem2d  13757  isacs2  13765  isacs1i  13769  invss  13873  ssctr  13912  funcres2b  13981  isacs3lem  14479  acsfiindd  14490  acsmapd  14491  acsmap2d  14492  tsrdir  14570  subsubm  14644  gsumwspan  14678  subsubg  14850  subgint  14851  cntzidss  15023  pgpssslw  15135  lsmless1x  15165  lsmless2x  15166  lsmless12  15182  subglsm  15192  gsumval3  15401  gsumzadd  15414  gsum2d  15433  dmdprdd  15447  dprdfeq0  15467  dprdspan  15472  dprdres  15473  dprdss  15474  dprdz  15475  subgdmdprd  15479  subgdprd  15480  dprdsn  15481  dprd2dlem1  15486  dprd2da  15487  dmdprdsplit2lem  15490  dprdsplit  15493  pgpfac1lem2  15520  pgpfac1lem3  15522  pgpfac1lem5  15524  subsubrg  15781  lspss  15951  lspun  15954  lsslsp  15982  lmhmlsp  16016  lsmelval2  16048  lsmssspx  16051  lsppratlem2  16111  lsppratlem3  16112  lsppratlem4  16113  lbsextlem2  16122  lbsextlem3  16123  aspss  16282  ocvlsp  16793  cssmre  16810  obselocv  16845  obslbs  16847  toponmre  17047  neiint  17058  neiss  17063  lpss  17091  lpss3  17093  restopnb  17123  restfpw  17127  restcls  17128  restntr  17129  restlp  17130  ordtbas  17139  pnfnei  17167  mnfnei  17168  cnclsi  17218  isreg2  17322  discmp  17342  cmpcld  17346  uncmp  17347  sscmp  17349  hauscmplem  17350  cmpfi  17352  iunconlem  17370  clscon  17373  2ndcctbss  17398  restnlly  17425  llyrest  17428  nllyrest  17429  llyidm  17431  nllyidm  17432  cldllycmp  17438  dislly  17440  llycmpkgen2  17462  ptbasfi  17493  txnlly  17548  txcmplem1  17552  tx1stc  17561  xkococnlem  17570  qtopval2  17604  basqtop  17619  tgqtop  17620  qtoprest  17625  kqreglem1  17649  kqreglem2  17650  kqnrmlem1  17651  kqnrmlem2  17652  fsubbas  17775  fgabs  17787  fbasrn  17792  trfil2  17795  trfg  17799  isufil2  17816  trufil  17818  ssufl  17826  ufileu  17827  filufint  17828  fmfnfmlem4  17865  fmfnfm  17866  flimss2  17880  flimss1  17881  fclsfnflim  17935  flimfnfcls  17936  fclscmp  17938  cnpfcfi  17948  alexsubALT  17958  clssubg  18004  clsnsg  18005  blss  18185  blcld  18264  blsscls  18266  met1stc  18280  met2ndci  18281  tgqioo  18519  xrsblre  18530  reconnlem2  18546  xrge0gsumle  18552  xrge0tsms  18553  rescncf  18615  cnmpt2pc  18641  cnheibor  18668  cnllycmp  18669  lebnum  18677  phtpycn  18696  cfilfcls  18915  iscmet3lem2  18933  cmetss  18955  cncmet  18959  bcthlem4  18964  bcth3  18968  minveclem4a  19009  minveclem4  19011  ivthicc  19033  ovollb  19053  ovollb2lem  19062  ovollb2  19063  nulmbl2  19109  ioorcl2  19142  uniioombllem3  19155  uniioombllem4  19156  uniioombllem5  19157  opnmbllem  19171  volcn  19176  volivth  19177  mbfeqalem  19212  itg10a  19280  mbfi1fseqlem4  19288  ditgcl  19423  ditgswap  19424  ditgsplitlem  19425  limcflf  19446  limcres  19451  dvbss  19466  dvbsss  19467  perfdvf  19468  dvreslem  19474  dvres2lem  19475  dvres3  19478  dvcnp  19483  dvcnp2  19484  dvcn  19485  dvnff  19487  dvn2bss  19494  dvnres  19495  cpnord  19499  dvaddbr  19502  dvmulbr  19503  dvaddf  19506  dvmulf  19507  dvcobr  19510  dvcof  19512  dvnfre  19516  dvmptres2  19526  dvmptntr  19535  dvcnvlem  19538  dvcnv  19539  dvferm1lem  19546  dvferm2lem  19548  dvlip  19555  dvlipcn  19556  dvlip2  19557  c1liplem1  19558  dvgt0lem1  19564  lhop1lem  19575  lhop  19578  dvcnvrelem1  19579  dvcnvrelem2  19580  dvcnvre  19581  dvfsumle  19583  dvfsumge  19584  dvfsumabs  19585  ftc1lem1  19597  ftc1lem2  19598  ftc1a  19599  ftc1lem4  19601  ftc2ditglem  19607  itgsubstlem  19610  ig1peu  19772  ig1pdvds  19777  taylfvallem1  19951  tayl0  19956  taylply2  19962  taylply  19963  dvtaylp  19964  dvntaylp  19965  dvntaylp0  19966  taylthlem1  19967  ulmdvlem1  19994  ulmdvlem3  19996  psercn  20020  pserdvlem2  20022  abelth  20035  xrlimcnp  20485  wilthlem2  20530  sqff1o  20643  chtublem  20673  pntlemq  20973  pntlemf  20977  ghsubgolem  21469  shintcli  22342  shub1  22395  mdslmd1lem1  23339  mdexchi  23349  chirredlem1  23404  mdsymlem5  23421  sumdmdii  23429  sumdmdlem2  23433  xrsupssd  23646  xrge0tsmsd  23735  neiptoptop  23764  iscnp4  23767  pnfneige0  23812  ustexsym  23841  ustund  23846  ustneism  23847  trust  23853  utoptop  23858  restutopopn  23862  metust  23922  cfilucfil  23923  restmetu  23935  sigaclci  24101  insiga  24106  sssigagen2  24115  dya2iocnei  24216  lgamucov  24391  erdszelem7  24452  erdszelem8  24453  erdsze2lem1  24458  conpcon  24490  cvmliftmolem1  24536  cvmlift2lem1  24557  cvmlift2lem9  24566  cvmlift2lem10  24567  cvmlift3lem6  24579  cvmlift3lem7  24580  rtrclreclem.min  24716  prodss  24842  dftrpred3g  25062  nofulllem3  25184  ontgval  25697  comppfsc  25899  neibastop2lem  25901  fnemeet2  25908  fnejoin1  25909  sstotbnd2  26089  heiborlem1  26126  heiborlem8  26133  intidl  26245  elrfi  26360  ismrcd1  26364  istopclsd  26366  mrefg2  26373  aomclem2  26743  aomclem6  26747  hbtlem6  26924  hbt  26925  symggen  27002  stoweidlem34  27374  bnj906  28714  bnj1020  28747  bnj1137  28777  bnj1408  28818  bnj1452  28834  lsmsat  29257  lssats  29261  lpssat  29262  lssatle  29264  lssat  29265  lsatcvatlem  29298  paddss12  30067  paddasslem17  30084  pmodlem1  30094  pmod1i  30096  pmodl42N  30099  elpcliN  30141  pclfinN  30148  polcon3N  30165  polcon2N  30167  paddunN  30175  pclfinclN  30198  poml5N  30202  osumcllem1N  30204  osumcllem2N  30205  osumcllem3N  30206  pl42lem2N  30228  pl42lem4N  30230  cdlemn5pre  31449  dihord1  31467  dihord2a  31468  dihord2b  31469  dihord5b  31508  dochss  31614  dochdmj1  31639  djhsumss  31656  djhunssN  31658  dochexmidlem2  31710  lclkrslem1  31786  lclkrslem2  31787  lcfrlem2  31792
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-in 3245  df-ss 3252
  Copyright terms: Public domain W3C validator