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

Theorem sstrd 3514
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 3512 . 2  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  syl5ss  3515  syl6ss  3516  ssdif2d  3643  uniintsn  4319  funss  5604  fssxp  5741  knatar  6239  suppssfvOLD  6513  suppssov1OLD  6514  tfisi  6671  suppfnss  6922  suppssov1  6929  suppssfv  6933  tposss  6953  tfrlem1  7042  omwordri  7218  oewordri  7238  oeeui  7248  oaabs2  7291  omopthlem1  7301  ecinxp  7383  sbthlem1  7624  dffi2  7879  hartogslem1  7963  cantnfcl  8082  cantnflt  8087  cantnfp1lem3  8095  cantnflem3  8106  cantnfclOLD  8112  cantnfltOLD  8117  cantnfp1lem3OLD  8121  cantnflem3OLD  8128  cnfcom  8140  cnfcom3lem  8143  cnfcomOLD  8148  cnfcom3lemOLD  8151  rankssb  8262  tskwe  8327  dfac12lem2  8520  dfac12lem3  8521  cfflb  8635  cfcof  8650  ssfin2  8696  hsmexlem4  8805  ttukeylem6  8890  ttukeylem7  8891  fpwwe2lem1  9005  fpwwe2lem8  9011  fpwwe2lem11  9014  fpwwe2lem12  9015  canthnumlem  9022  canthwelem  9024  canthwe  9025  canthp1lem2  9027  pwfseqlem5  9037  wunex2  9112  tsktrss  9135  inttsk  9148  uzwo3  11173  supicc  11664  supiccub  11665  supicclub  11666  seqsplit  12103  seqf1olem2a  12108  seqz  12118  swrdval2  12604  sumss  13502  qshash  13595  incexc  13605  incexc2  13606  rpnnen2lem11  13812  vdwlem1  14351  ramub1lem1  14396  imasaddvallem  14777  imasvscaf  14787  mrerintcl  14845  ismred2  14851  mremre  14852  mrcuni  14869  mressmrcd  14875  submrc  14876  mrissmrid  14889  mreexexlem2d  14893  isacs2  14901  isacs1i  14905  invss  15009  ssctr  15048  funcres2b  15117  isacs3lem  15646  acsfiindd  15657  acsmapd  15658  acsmap2d  15659  tsrdir  15718  subsubm  15795  gsumwspan  15834  subsubg  16016  subgint  16017  cntzidss  16167  symggen  16288  pmtrdifellem1  16294  pmtrdifellem2  16295  pgpssslw  16427  lsmless1x  16457  lsmless2x  16458  lsmless12  16474  subglsm  16484  gsumval3OLD  16696  gsumval3lem2  16698  gsumzaddlem  16722  gsumzadd  16723  gsumzaddOLD  16725  gsumconst  16742  gsum2d  16787  gsum2dOLD  16788  dmdprdd  16818  dprdfeq0  16849  dprdfeq0OLD  16856  dprdspan  16861  dprdres  16862  dprdss  16863  dprdz  16864  subgdmdprd  16868  subgdprd  16869  dprdsn  16870  dprd2dlem1  16877  dprd2da  16878  dmdprdsplit2lem  16881  dprdsplit  16884  pgpfac1lem2  16913  pgpfac1lem3  16915  pgpfac1lem5  16917  subsubrg  17235  lspss  17410  lspun  17413  lsslsp  17441  lmhmlsp  17475  lsmelval2  17511  lsmssspx  17514  lsppratlem2  17574  lsppratlem3  17575  lsppratlem4  17576  lbsextlem2  17585  lbsextlem3  17586  aspss  17749  ocvlsp  18471  cssmre  18488  obselocv  18523  obslbs  18525  toponmre  19357  neiint  19368  neiss  19373  lpss  19406  lpss3  19408  restopnb  19439  restfpw  19443  neitr  19444  restcls  19445  restntr  19446  restlp  19447  ordtbas  19456  pnfnei  19484  mnfnei  19485  iscnp4  19527  cnclsi  19536  isreg2  19641  discmp  19661  cmpcld  19665  uncmp  19666  sscmp  19668  hauscmplem  19669  cmpfi  19671  iunconlem  19691  clscon  19694  2ndcctbss  19719  restnlly  19746  llyrest  19749  nllyrest  19750  llyidm  19752  nllyidm  19753  cldllycmp  19759  dislly  19761  llycmpkgen2  19783  ptbasfi  19814  txnlly  19870  txcmplem1  19874  tx1stc  19883  xkococnlem  19892  qtopval2  19929  basqtop  19944  tgqtop  19945  qtoprest  19950  kqreglem1  19974  kqreglem2  19975  kqnrmlem1  19976  kqnrmlem2  19977  fsubbas  20100  fgabs  20112  fbasrn  20117  trfil2  20120  trfg  20124  isufil2  20141  trufil  20143  ssufl  20151  ufileu  20152  filufint  20153  fmfnfmlem4  20190  fmfnfm  20191  flimss2  20205  flimss1  20206  fclsfnflim  20260  flimfnfcls  20261  fclscmp  20263  cnpfcfi  20273  alexsubALT  20283  clssubg  20339  clsnsg  20340  tsmsres  20378  ustexsym  20450  ustex2sym  20451  ustex3sym  20452  ustund  20456  ustneism  20458  trust  20464  utoptop  20469  restutopopn  20473  utop2nei  20485  utopreg  20487  cfiluweak  20530  neipcfilu  20531  blssps  20659  blss  20660  blcld  20740  blsscls  20742  met1stc  20756  met2ndci  20757  metustOLD  20802  metust  20803  cfilucfilOLD  20804  cfilucfil  20805  restmetu  20822  tgqioo  21037  xrsblre  21048  reconnlem2  21064  xrge0gsumle  21070  xrge0tsms  21071  rescncf  21133  cnmpt2pc  21160  cnheibor  21187  cnllycmp  21188  lebnum  21196  phtpycn  21215  cfilfcls  21445  iscmet3lem2  21463  cmetss  21485  cncmet  21493  bcthlem4  21498  bcth3  21502  rrxcph  21556  rrxmetlem  21566  minveclem4a  21577  minveclem4  21579  ivthicc  21602  ovollb  21622  ovollb2lem  21631  ovollb2  21632  nulmbl2  21679  ioorcl2  21713  uniioombllem3  21726  uniioombllem4  21727  uniioombllem5  21728  opnmbllem  21742  volcn  21747  volivth  21748  mbfeqalem  21781  itg10a  21849  mbfi1fseqlem4  21857  ditgcl  21994  ditgswap  21995  ditgsplitlem  21996  limcflf  22017  limcres  22022  dvbss  22037  dvbsss  22038  perfdvf  22039  dvreslem  22045  dvres2lem  22046  dvres3  22049  dvcnp  22054  dvcnp2  22055  dvcn  22056  dvnff  22058  dvn2bss  22065  dvnres  22066  cpnord  22070  dvaddbr  22073  dvmulbr  22074  dvcobr  22081  dvnfre  22087  dvmptres2  22097  dvmptntr  22106  dvcnvlem  22109  dvcnv  22110  dvferm1lem  22117  dvferm2lem  22119  dvlip  22126  dvlipcn  22127  dvlip2  22128  c1liplem1  22129  dvgt0lem1  22135  lhop1lem  22146  lhop  22149  dvcnvrelem1  22150  dvcnvrelem2  22151  dvcnvre  22152  dvfsumle  22154  dvfsumge  22155  dvfsumabs  22156  ftc1lem1  22168  ftc1lem2  22169  ftc1a  22170  ftc1lem4  22172  ftc2ditglem  22178  itgsubstlem  22181  ig1peu  22304  ig1pdvds  22309  taylfvallem1  22483  tayl0  22488  taylply2  22494  taylply  22495  dvtaylp  22496  dvntaylp  22497  dvntaylp0  22498  taylthlem1  22499  ulmdvlem1  22526  ulmdvlem3  22528  psercn  22552  pserdvlem2  22554  abelth  22567  xrlimcnp  23023  wilthlem2  23068  sqff1o  23181  chtublem  23211  pntlemq  23511  pntlemf  23515  tglineintmo  23732  ttgcontlem1  23861  ghsubgolem  25045  shintcli  25920  shub1  25973  mdslmd1lem1  26917  mdexchi  26927  chirredlem1  26982  mdsymlem5  26999  sumdmdii  27007  sumdmdlem2  27011  ofpreima2  27177  xrsupssd  27244  xrge0infssd  27246  xrge0tsmsd  27435  pnfneige0  27566  insiga  27774  sssigagen2  27783  dya2iocnei  27890  omsmon  27904  lgamucov  28217  erdszelem7  28278  erdszelem8  28279  erdsze2lem1  28284  conpcon  28317  cvmliftmolem1  28363  cvmlift2lem1  28384  cvmlift2lem9  28393  cvmlift2lem10  28394  cvmlift3lem6  28406  cvmlift3lem7  28407  rtrclreclem.min  28542  prodss  28653  dftrpred3g  28890  nofulllem3  29038  ontgval  29470  opnmbllem0  29625  ftc1anclem7  29671  ftc1anclem8  29672  ftc1anc  29673  comppfsc  29777  neibastop2lem  29779  fnemeet2  29786  fnejoin1  29787  sstotbnd2  29871  heiborlem1  29908  heiborlem8  29915  intidl  30027  elrfi  30228  ismrcd1  30232  istopclsd  30234  mrefg2  30241  aomclem2  30605  aomclem6  30609  hbtlem6  30682  hbt  30683  limccog  31162  limciccioolb  31163  limcicciooub  31179  limclner  31193  cncfmptssg  31208  cncfuni  31225  icccncfext  31226  cncfiooicclem1  31232  dvresntr  31246  dvmptresicc  31249  dvbdfbdioolem1  31258  itgcoscmulx  31287  itgsincmulx  31292  itgsubsticclem  31293  itgiccshift  31298  itgperiod  31299  itgsbtaddcnst  31300  stoweidlem59  31359  dirkercncflem2  31404  fourierdlem20  31427  fourierdlem38  31445  fourierdlem39  31446  fourierdlem42  31449  fourierdlem48  31455  fourierdlem49  31456  fourierdlem51  31458  fourierdlem52  31459  fourierdlem58  31465  fourierdlem63  31470  fourierdlem64  31471  fourierdlem69  31476  fourierdlem70  31477  fourierdlem73  31480  fourierdlem74  31481  fourierdlem75  31482  fourierdlem76  31483  fourierdlem80  31487  fourierdlem84  31491  fourierdlem85  31492  fourierdlem88  31495  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem93  31500  fourierdlem94  31501  fourierdlem100  31507  fourierdlem103  31510  fourierdlem104  31511  fourierdlem107  31514  fourierdlem111  31518  fourierdlem112  31519  fourierdlem113  31520  fouriersw  31532  bnj906  33067  bnj1020  33100  bnj1137  33130  bnj1408  33171  bnj1452  33187  lsmsat  33805  lssats  33809  lpssat  33810  lssatle  33812  lssat  33813  lsatcvatlem  33846  paddss12  34615  paddasslem17  34632  pmodlem1  34642  pmod1i  34644  pmodl42N  34647  elpcliN  34689  pclfinN  34696  polcon3N  34713  polcon2N  34715  paddunN  34723  pclfinclN  34746  poml5N  34750  osumcllem1N  34752  osumcllem2N  34753  osumcllem3N  34754  pl42lem2N  34776  pl42lem4N  34778  cdlemn5pre  35997  dihord1  36015  dihord2a  36016  dihord2b  36017  dihord5b  36056  dochss  36162  dochdmj1  36187  djhsumss  36204  djhunssN  36206  dochexmidlem2  36258  lclkrslem1  36334  lclkrslem2  36335  lcfrlem2  36340  trrelssd  36787
  Copyright terms: Public domain W3C validator