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

Theorem sstrd 3345
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 3343 . 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 3307
This theorem is referenced by:  syl5ss  3346  syl6ss  3347  ssdif2d  3473  uniintsn  4074  tfisi  4824  funss  5458  fssxp  5588  knatar  6066  suppssfv  6287  suppssov1  6288  tposss  6466  omwordri  6801  oewordri  6821  oeeui  6831  oaabs2  6874  omopthlem1  6884  ecinxp  6965  sbthlem1  7203  dffi2  7414  hartogslem1  7495  cantnfcl  7606  cantnflt  7611  cantnfp1lem3  7620  cantnflem3  7631  cnfcom  7641  cnfcom3lem  7644  rankssb  7758  tskwe  7821  dfac12lem2  8008  dfac12lem3  8009  cfflb  8123  cfcof  8138  ssfin2  8184  hsmexlem4  8293  ttukeylem6  8378  ttukeylem7  8379  fpwwe2lem1  8490  fpwwe2lem8  8496  fpwwe2lem11  8499  fpwwe2lem12  8500  canthnumlem  8507  canthwelem  8509  canthwe  8510  canthp1lem2  8512  pwfseqlem5  8522  wunex2  8597  tsktrss  8620  inttsk  8633  uzwo3  10553  seqsplit  11339  seqf1olem2a  11344  seqz  11354  swrdval2  11750  sumss  12501  qshash  12589  incexc  12600  incexc2  12601  rpnnen2lem11  12807  vdwlem1  13332  ramub1lem1  13377  imasaddvallem  13737  imasvscaf  13747  mrerintcl  13805  ismred2  13811  mremre  13812  mrcuni  13829  mressmrcd  13835  submrc  13836  mrissmrid  13849  mreexexlem2d  13853  isacs2  13861  isacs1i  13865  invss  13969  ssctr  14008  funcres2b  14077  isacs3lem  14575  acsfiindd  14586  acsmapd  14587  acsmap2d  14588  tsrdir  14666  subsubm  14740  gsumwspan  14774  subsubg  14946  subgint  14947  cntzidss  15119  pgpssslw  15231  lsmless1x  15261  lsmless2x  15262  lsmless12  15278  subglsm  15288  gsumval3  15497  gsumzadd  15510  gsum2d  15529  dmdprdd  15543  dprdfeq0  15563  dprdspan  15568  dprdres  15569  dprdss  15570  dprdz  15571  subgdmdprd  15575  subgdprd  15576  dprdsn  15577  dprd2dlem1  15582  dprd2da  15583  dmdprdsplit2lem  15586  dprdsplit  15589  pgpfac1lem2  15616  pgpfac1lem3  15618  pgpfac1lem5  15620  subsubrg  15877  lspss  16043  lspun  16046  lsslsp  16074  lmhmlsp  16108  lsmelval2  16140  lsmssspx  16143  lsppratlem2  16203  lsppratlem3  16204  lsppratlem4  16205  lbsextlem2  16214  lbsextlem3  16215  aspss  16374  ocvlsp  16886  cssmre  16903  obselocv  16938  obslbs  16940  toponmre  17140  neiint  17151  neiss  17156  lpss  17189  lpss3  17191  restopnb  17222  restfpw  17226  neitr  17227  restcls  17228  restntr  17229  restlp  17230  ordtbas  17239  pnfnei  17267  mnfnei  17268  iscnp4  17310  cnclsi  17319  isreg2  17424  discmp  17444  cmpcld  17448  uncmp  17449  sscmp  17451  hauscmplem  17452  cmpfi  17454  iunconlem  17473  clscon  17476  2ndcctbss  17501  restnlly  17528  llyrest  17531  nllyrest  17532  llyidm  17534  nllyidm  17535  cldllycmp  17541  dislly  17543  llycmpkgen2  17565  ptbasfi  17596  txnlly  17652  txcmplem1  17656  tx1stc  17665  xkococnlem  17674  qtopval2  17711  basqtop  17726  tgqtop  17727  qtoprest  17732  kqreglem1  17756  kqreglem2  17757  kqnrmlem1  17758  kqnrmlem2  17759  fsubbas  17882  fgabs  17894  fbasrn  17899  trfil2  17902  trfg  17906  isufil2  17923  trufil  17925  ssufl  17933  ufileu  17934  filufint  17935  fmfnfmlem4  17972  fmfnfm  17973  flimss2  17987  flimss1  17988  fclsfnflim  18042  flimfnfcls  18043  fclscmp  18045  cnpfcfi  18055  alexsubALT  18065  clssubg  18121  clsnsg  18122  ustexsym  18228  ustex2sym  18229  ustex3sym  18230  ustund  18234  ustneism  18236  trust  18242  utoptop  18247  restutopopn  18251  utop2nei  18263  utopreg  18265  cfiluweak  18308  neipcfilu  18309  blssps  18437  blss  18438  blcld  18518  blsscls  18520  met1stc  18534  met2ndci  18535  metustOLD  18580  metust  18581  cfilucfilOLD  18582  cfilucfil  18583  restmetu  18600  tgqioo  18814  xrsblre  18825  reconnlem2  18841  xrge0gsumle  18847  xrge0tsms  18848  rescncf  18910  cnmpt2pc  18936  cnheibor  18963  cnllycmp  18964  lebnum  18972  phtpycn  18991  cfilfcls  19210  iscmet3lem2  19228  cmetss  19250  cncmet  19258  bcthlem4  19263  bcth3  19267  minveclem4a  19314  minveclem4  19316  ivthicc  19338  ovollb  19358  ovollb2lem  19367  ovollb2  19368  nulmbl2  19414  ioorcl2  19447  uniioombllem3  19460  uniioombllem4  19461  uniioombllem5  19462  opnmbllem  19476  volcn  19481  volivth  19482  mbfeqalem  19517  itg10a  19585  mbfi1fseqlem4  19593  ditgcl  19728  ditgswap  19729  ditgsplitlem  19730  limcflf  19751  limcres  19756  dvbss  19771  dvbsss  19772  perfdvf  19773  dvreslem  19779  dvres2lem  19780  dvres3  19783  dvcnp  19788  dvcnp2  19789  dvcn  19790  dvnff  19792  dvn2bss  19799  dvnres  19800  cpnord  19804  dvaddbr  19807  dvmulbr  19808  dvcobr  19815  dvnfre  19821  dvmptres2  19831  dvmptntr  19840  dvcnvlem  19843  dvcnv  19844  dvferm1lem  19851  dvferm2lem  19853  dvlip  19860  dvlipcn  19861  dvlip2  19862  c1liplem1  19863  dvgt0lem1  19869  lhop1lem  19880  lhop  19883  dvcnvrelem1  19884  dvcnvrelem2  19885  dvcnvre  19886  dvfsumle  19888  dvfsumge  19889  dvfsumabs  19890  ftc1lem1  19902  ftc1lem2  19903  ftc1a  19904  ftc1lem4  19906  ftc2ditglem  19912  itgsubstlem  19915  ig1peu  20077  ig1pdvds  20082  taylfvallem1  20256  tayl0  20261  taylply2  20267  taylply  20268  dvtaylp  20269  dvntaylp  20270  dvntaylp0  20271  taylthlem1  20272  ulmdvlem1  20299  ulmdvlem3  20301  psercn  20325  pserdvlem2  20327  abelth  20340  xrlimcnp  20790  wilthlem2  20835  sqff1o  20948  chtublem  20978  pntlemq  21278  pntlemf  21282  ghsubgolem  21941  shintcli  22814  shub1  22867  mdslmd1lem1  23811  mdexchi  23821  chirredlem1  23876  mdsymlem5  23893  sumdmdii  23901  sumdmdlem2  23905  xrsupssd  24108  xrge0tsmsd  24206  pnfneige0  24319  insiga  24503  sssigagen2  24512  dya2iocnei  24615  sibfof  24637  lgamucov  24805  erdszelem7  24866  erdszelem8  24867  erdsze2lem1  24872  conpcon  24905  cvmliftmolem1  24951  cvmlift2lem1  24972  cvmlift2lem9  24981  cvmlift2lem10  24982  cvmlift3lem6  24994  cvmlift3lem7  24995  rtrclreclem.min  25130  prodss  25257  dftrpred3g  25486  nofulllem3  25608  ontgval  26124  mblfinlem  26185  comppfsc  26319  neibastop2lem  26321  fnemeet2  26328  fnejoin1  26329  sstotbnd2  26415  heiborlem1  26452  heiborlem8  26459  intidl  26571  elrfi  26680  ismrcd1  26684  istopclsd  26686  mrefg2  26693  aomclem2  27062  aomclem6  27066  hbtlem6  27243  hbt  27244  symggen  27321  stoweidlem59  27717  bnj906  29053  bnj1020  29086  bnj1137  29116  bnj1408  29157  bnj1452  29173  lsmsat  29537  lssats  29541  lpssat  29542  lssatle  29544  lssat  29545  lsatcvatlem  29578  paddss12  30347  paddasslem17  30364  pmodlem1  30374  pmod1i  30376  pmodl42N  30379  elpcliN  30421  pclfinN  30428  polcon3N  30445  polcon2N  30447  paddunN  30455  pclfinclN  30478  poml5N  30482  osumcllem1N  30484  osumcllem2N  30485  osumcllem3N  30486  pl42lem2N  30508  pl42lem4N  30510  cdlemn5pre  31729  dihord1  31747  dihord2a  31748  dihord2b  31749  dihord5b  31788  dochss  31894  dochdmj1  31919  djhsumss  31936  djhunssN  31938  dochexmidlem2  31990  lclkrslem1  32066  lclkrslem2  32067  lcfrlem2  32072
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 2411
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 2417  df-cleq 2423  df-clel 2426  df-in 3314  df-ss 3321
  Copyright terms: Public domain W3C validator