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

Theorem sstrd 3360
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 3358 . 2  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
41, 2, 3syl2anc 644 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3322
This theorem is referenced by:  syl5ss  3361  syl6ss  3362  ssdif2d  3488  uniintsn  4089  tfisi  4841  funss  5475  fssxp  5605  knatar  6083  suppssfv  6304  suppssov1  6305  tposss  6483  omwordri  6818  oewordri  6838  oeeui  6848  oaabs2  6891  omopthlem1  6901  ecinxp  6982  sbthlem1  7220  dffi2  7431  hartogslem1  7514  cantnfcl  7625  cantnflt  7630  cantnfp1lem3  7639  cantnflem3  7650  cnfcom  7660  cnfcom3lem  7663  rankssb  7777  tskwe  7842  dfac12lem2  8029  dfac12lem3  8030  cfflb  8144  cfcof  8159  ssfin2  8205  hsmexlem4  8314  ttukeylem6  8399  ttukeylem7  8400  fpwwe2lem1  8511  fpwwe2lem8  8517  fpwwe2lem11  8520  fpwwe2lem12  8521  canthnumlem  8528  canthwelem  8530  canthwe  8531  canthp1lem2  8533  pwfseqlem5  8543  wunex2  8618  tsktrss  8641  inttsk  8654  uzwo3  10574  seqsplit  11361  seqf1olem2a  11366  seqz  11376  swrdval2  11772  sumss  12523  qshash  12611  incexc  12622  incexc2  12623  rpnnen2lem11  12829  vdwlem1  13354  ramub1lem1  13399  imasaddvallem  13759  imasvscaf  13769  mrerintcl  13827  ismred2  13833  mremre  13834  mrcuni  13851  mressmrcd  13857  submrc  13858  mrissmrid  13871  mreexexlem2d  13875  isacs2  13883  isacs1i  13887  invss  13991  ssctr  14030  funcres2b  14099  isacs3lem  14597  acsfiindd  14608  acsmapd  14609  acsmap2d  14610  tsrdir  14688  subsubm  14762  gsumwspan  14796  subsubg  14968  subgint  14969  cntzidss  15141  pgpssslw  15253  lsmless1x  15283  lsmless2x  15284  lsmless12  15300  subglsm  15310  gsumval3  15519  gsumzadd  15532  gsum2d  15551  dmdprdd  15565  dprdfeq0  15585  dprdspan  15590  dprdres  15591  dprdss  15592  dprdz  15593  subgdmdprd  15597  subgdprd  15598  dprdsn  15599  dprd2dlem1  15604  dprd2da  15605  dmdprdsplit2lem  15608  dprdsplit  15611  pgpfac1lem2  15638  pgpfac1lem3  15640  pgpfac1lem5  15642  subsubrg  15899  lspss  16065  lspun  16068  lsslsp  16096  lmhmlsp  16130  lsmelval2  16162  lsmssspx  16165  lsppratlem2  16225  lsppratlem3  16226  lsppratlem4  16227  lbsextlem2  16236  lbsextlem3  16237  aspss  16396  ocvlsp  16908  cssmre  16925  obselocv  16960  obslbs  16962  toponmre  17162  neiint  17173  neiss  17178  lpss  17211  lpss3  17213  restopnb  17244  restfpw  17248  neitr  17249  restcls  17250  restntr  17251  restlp  17252  ordtbas  17261  pnfnei  17289  mnfnei  17290  iscnp4  17332  cnclsi  17341  isreg2  17446  discmp  17466  cmpcld  17470  uncmp  17471  sscmp  17473  hauscmplem  17474  cmpfi  17476  iunconlem  17495  clscon  17498  2ndcctbss  17523  restnlly  17550  llyrest  17553  nllyrest  17554  llyidm  17556  nllyidm  17557  cldllycmp  17563  dislly  17565  llycmpkgen2  17587  ptbasfi  17618  txnlly  17674  txcmplem1  17678  tx1stc  17687  xkococnlem  17696  qtopval2  17733  basqtop  17748  tgqtop  17749  qtoprest  17754  kqreglem1  17778  kqreglem2  17779  kqnrmlem1  17780  kqnrmlem2  17781  fsubbas  17904  fgabs  17916  fbasrn  17921  trfil2  17924  trfg  17928  isufil2  17945  trufil  17947  ssufl  17955  ufileu  17956  filufint  17957  fmfnfmlem4  17994  fmfnfm  17995  flimss2  18009  flimss1  18010  fclsfnflim  18064  flimfnfcls  18065  fclscmp  18067  cnpfcfi  18077  alexsubALT  18087  clssubg  18143  clsnsg  18144  ustexsym  18250  ustex2sym  18251  ustex3sym  18252  ustund  18256  ustneism  18258  trust  18264  utoptop  18269  restutopopn  18273  utop2nei  18285  utopreg  18287  cfiluweak  18330  neipcfilu  18331  blssps  18459  blss  18460  blcld  18540  blsscls  18542  met1stc  18556  met2ndci  18557  metustOLD  18602  metust  18603  cfilucfilOLD  18604  cfilucfil  18605  restmetu  18622  tgqioo  18836  xrsblre  18847  reconnlem2  18863  xrge0gsumle  18869  xrge0tsms  18870  rescncf  18932  cnmpt2pc  18958  cnheibor  18985  cnllycmp  18986  lebnum  18994  phtpycn  19013  cfilfcls  19232  iscmet3lem2  19250  cmetss  19272  cncmet  19280  bcthlem4  19285  bcth3  19289  minveclem4a  19336  minveclem4  19338  ivthicc  19360  ovollb  19380  ovollb2lem  19389  ovollb2  19390  nulmbl2  19436  ioorcl2  19469  uniioombllem3  19482  uniioombllem4  19483  uniioombllem5  19484  opnmbllem  19498  volcn  19503  volivth  19504  mbfeqalem  19537  itg10a  19605  mbfi1fseqlem4  19613  ditgcl  19750  ditgswap  19751  ditgsplitlem  19752  limcflf  19773  limcres  19778  dvbss  19793  dvbsss  19794  perfdvf  19795  dvreslem  19801  dvres2lem  19802  dvres3  19805  dvcnp  19810  dvcnp2  19811  dvcn  19812  dvnff  19814  dvn2bss  19821  dvnres  19822  cpnord  19826  dvaddbr  19829  dvmulbr  19830  dvcobr  19837  dvnfre  19843  dvmptres2  19853  dvmptntr  19862  dvcnvlem  19865  dvcnv  19866  dvferm1lem  19873  dvferm2lem  19875  dvlip  19882  dvlipcn  19883  dvlip2  19884  c1liplem1  19885  dvgt0lem1  19891  lhop1lem  19902  lhop  19905  dvcnvrelem1  19906  dvcnvrelem2  19907  dvcnvre  19908  dvfsumle  19910  dvfsumge  19911  dvfsumabs  19912  ftc1lem1  19924  ftc1lem2  19925  ftc1a  19926  ftc1lem4  19928  ftc2ditglem  19934  itgsubstlem  19937  ig1peu  20099  ig1pdvds  20104  taylfvallem1  20278  tayl0  20283  taylply2  20289  taylply  20290  dvtaylp  20291  dvntaylp  20292  dvntaylp0  20293  taylthlem1  20294  ulmdvlem1  20321  ulmdvlem3  20323  psercn  20347  pserdvlem2  20349  abelth  20362  xrlimcnp  20812  wilthlem2  20857  sqff1o  20970  chtublem  21000  pntlemq  21300  pntlemf  21304  ghsubgolem  21963  shintcli  22836  shub1  22889  mdslmd1lem1  23833  mdexchi  23843  chirredlem1  23898  mdsymlem5  23915  sumdmdii  23923  sumdmdlem2  23927  xrsupssd  24130  xrge0tsmsd  24228  pnfneige0  24341  insiga  24525  sssigagen2  24534  dya2iocnei  24637  sibfof  24659  lgamucov  24827  erdszelem7  24888  erdszelem8  24889  erdsze2lem1  24894  conpcon  24927  cvmliftmolem1  24973  cvmlift2lem1  24994  cvmlift2lem9  25003  cvmlift2lem10  25004  cvmlift3lem6  25016  cvmlift3lem7  25017  rtrclreclem.min  25152  prodss  25278  dftrpred3g  25516  nofulllem3  25664  ontgval  26186  opnmbllem0  26254  ftc1anclem7  26300  ftc1anclem8  26301  ftc1anc  26302  comppfsc  26401  neibastop2lem  26403  fnemeet2  26410  fnejoin1  26411  sstotbnd2  26497  heiborlem1  26534  heiborlem8  26541  intidl  26653  elrfi  26762  ismrcd1  26766  istopclsd  26768  mrefg2  26775  aomclem2  27144  aomclem6  27148  hbtlem6  27324  hbt  27325  symggen  27402  stoweidlem59  27798  bnj906  29375  bnj1020  29408  bnj1137  29438  bnj1408  29479  bnj1452  29495  lsmsat  29880  lssats  29884  lpssat  29885  lssatle  29887  lssat  29888  lsatcvatlem  29921  paddss12  30690  paddasslem17  30707  pmodlem1  30717  pmod1i  30719  pmodl42N  30722  elpcliN  30764  pclfinN  30771  polcon3N  30788  polcon2N  30790  paddunN  30798  pclfinclN  30821  poml5N  30825  osumcllem1N  30827  osumcllem2N  30828  osumcllem3N  30829  pl42lem2N  30851  pl42lem4N  30853  cdlemn5pre  32072  dihord1  32090  dihord2a  32091  dihord2b  32092  dihord5b  32131  dochss  32237  dochdmj1  32262  djhsumss  32279  djhunssN  32281  dochexmidlem2  32333  lclkrslem1  32409  lclkrslem2  32410  lcfrlem2  32415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator