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

Theorem sstrd 3318
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 3316 . 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 3280
This theorem is referenced by:  syl5ss  3319  syl6ss  3320  ssdif2d  3446  uniintsn  4047  tfisi  4797  funss  5431  fssxp  5561  knatar  6039  suppssfv  6260  suppssov1  6261  tposss  6439  omwordri  6774  oewordri  6794  oeeui  6804  oaabs2  6847  omopthlem1  6857  ecinxp  6938  sbthlem1  7176  dffi2  7386  hartogslem1  7467  cantnfcl  7578  cantnflt  7583  cantnfp1lem3  7592  cantnflem3  7603  cnfcom  7613  cnfcom3lem  7616  rankssb  7730  tskwe  7793  dfac12lem2  7980  dfac12lem3  7981  cfflb  8095  cfcof  8110  ssfin2  8156  hsmexlem4  8265  ttukeylem6  8350  ttukeylem7  8351  fpwwe2lem1  8462  fpwwe2lem8  8468  fpwwe2lem11  8471  fpwwe2lem12  8472  canthnumlem  8479  canthwelem  8481  canthwe  8482  canthp1lem2  8484  pwfseqlem5  8494  wunex2  8569  tsktrss  8592  inttsk  8605  uzwo3  10525  seqsplit  11311  seqf1olem2a  11316  seqz  11326  swrdval2  11722  sumss  12473  qshash  12561  incexc  12572  incexc2  12573  rpnnen2lem11  12779  vdwlem1  13304  ramub1lem1  13349  imasaddvallem  13709  imasvscaf  13719  mrerintcl  13777  ismred2  13783  mremre  13784  mrcuni  13801  mressmrcd  13807  submrc  13808  mrissmrid  13821  mreexexlem2d  13825  isacs2  13833  isacs1i  13837  invss  13941  ssctr  13980  funcres2b  14049  isacs3lem  14547  acsfiindd  14558  acsmapd  14559  acsmap2d  14560  tsrdir  14638  subsubm  14712  gsumwspan  14746  subsubg  14918  subgint  14919  cntzidss  15091  pgpssslw  15203  lsmless1x  15233  lsmless2x  15234  lsmless12  15250  subglsm  15260  gsumval3  15469  gsumzadd  15482  gsum2d  15501  dmdprdd  15515  dprdfeq0  15535  dprdspan  15540  dprdres  15541  dprdss  15542  dprdz  15543  subgdmdprd  15547  subgdprd  15548  dprdsn  15549  dprd2dlem1  15554  dprd2da  15555  dmdprdsplit2lem  15558  dprdsplit  15561  pgpfac1lem2  15588  pgpfac1lem3  15590  pgpfac1lem5  15592  subsubrg  15849  lspss  16015  lspun  16018  lsslsp  16046  lmhmlsp  16080  lsmelval2  16112  lsmssspx  16115  lsppratlem2  16175  lsppratlem3  16176  lsppratlem4  16177  lbsextlem2  16186  lbsextlem3  16187  aspss  16346  ocvlsp  16858  cssmre  16875  obselocv  16910  obslbs  16912  toponmre  17112  neiint  17123  neiss  17128  lpss  17161  lpss3  17163  restopnb  17193  restfpw  17197  neitr  17198  restcls  17199  restntr  17200  restlp  17201  ordtbas  17210  pnfnei  17238  mnfnei  17239  iscnp4  17281  cnclsi  17290  isreg2  17395  discmp  17415  cmpcld  17419  uncmp  17420  sscmp  17422  hauscmplem  17423  cmpfi  17425  iunconlem  17443  clscon  17446  2ndcctbss  17471  restnlly  17498  llyrest  17501  nllyrest  17502  llyidm  17504  nllyidm  17505  cldllycmp  17511  dislly  17513  llycmpkgen2  17535  ptbasfi  17566  txnlly  17622  txcmplem1  17626  tx1stc  17635  xkococnlem  17644  qtopval2  17681  basqtop  17696  tgqtop  17697  qtoprest  17702  kqreglem1  17726  kqreglem2  17727  kqnrmlem1  17728  kqnrmlem2  17729  fsubbas  17852  fgabs  17864  fbasrn  17869  trfil2  17872  trfg  17876  isufil2  17893  trufil  17895  ssufl  17903  ufileu  17904  filufint  17905  fmfnfmlem4  17942  fmfnfm  17943  flimss2  17957  flimss1  17958  fclsfnflim  18012  flimfnfcls  18013  fclscmp  18015  cnpfcfi  18025  alexsubALT  18035  clssubg  18091  clsnsg  18092  ustexsym  18198  ustex2sym  18199  ustex3sym  18200  ustund  18204  ustneism  18206  trust  18212  utoptop  18217  restutopopn  18221  utop2nei  18233  utopreg  18235  cfiluweak  18278  neipcfilu  18279  blssps  18407  blss  18408  blcld  18488  blsscls  18490  met1stc  18504  met2ndci  18505  metustOLD  18550  metust  18551  cfilucfilOLD  18552  cfilucfil  18553  restmetu  18570  tgqioo  18784  xrsblre  18795  reconnlem2  18811  xrge0gsumle  18817  xrge0tsms  18818  rescncf  18880  cnmpt2pc  18906  cnheibor  18933  cnllycmp  18934  lebnum  18942  phtpycn  18961  cfilfcls  19180  iscmet3lem2  19198  cmetss  19220  cncmet  19228  bcthlem4  19233  bcth3  19237  minveclem4a  19284  minveclem4  19286  ivthicc  19308  ovollb  19328  ovollb2lem  19337  ovollb2  19338  nulmbl2  19384  ioorcl2  19417  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  opnmbllem  19446  volcn  19451  volivth  19452  mbfeqalem  19487  itg10a  19555  mbfi1fseqlem4  19563  ditgcl  19698  ditgswap  19699  ditgsplitlem  19700  limcflf  19721  limcres  19726  dvbss  19741  dvbsss  19742  perfdvf  19743  dvreslem  19749  dvres2lem  19750  dvres3  19753  dvcnp  19758  dvcnp2  19759  dvcn  19760  dvnff  19762  dvn2bss  19769  dvnres  19770  cpnord  19774  dvaddbr  19777  dvmulbr  19778  dvcobr  19785  dvnfre  19791  dvmptres2  19801  dvmptntr  19810  dvcnvlem  19813  dvcnv  19814  dvferm1lem  19821  dvferm2lem  19823  dvlip  19830  dvlipcn  19831  dvlip2  19832  c1liplem1  19833  dvgt0lem1  19839  lhop1lem  19850  lhop  19853  dvcnvrelem1  19854  dvcnvrelem2  19855  dvcnvre  19856  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  ftc1lem1  19872  ftc1lem2  19873  ftc1a  19874  ftc1lem4  19876  ftc2ditglem  19882  itgsubstlem  19885  ig1peu  20047  ig1pdvds  20052  taylfvallem1  20226  tayl0  20231  taylply2  20237  taylply  20238  dvtaylp  20239  dvntaylp  20240  dvntaylp0  20241  taylthlem1  20242  ulmdvlem1  20269  ulmdvlem3  20271  psercn  20295  pserdvlem2  20297  abelth  20310  xrlimcnp  20760  wilthlem2  20805  sqff1o  20918  chtublem  20948  pntlemq  21248  pntlemf  21252  ghsubgolem  21911  shintcli  22784  shub1  22837  mdslmd1lem1  23781  mdexchi  23791  chirredlem1  23846  mdsymlem5  23863  sumdmdii  23871  sumdmdlem2  23875  xrsupssd  24078  xrge0tsmsd  24176  pnfneige0  24289  insiga  24473  sssigagen2  24482  dya2iocnei  24585  sibfof  24607  lgamucov  24775  erdszelem7  24836  erdszelem8  24837  erdsze2lem1  24842  conpcon  24875  cvmliftmolem1  24921  cvmlift2lem1  24942  cvmlift2lem9  24951  cvmlift2lem10  24952  cvmlift3lem6  24964  cvmlift3lem7  24965  rtrclreclem.min  25100  prodss  25226  dftrpred3g  25450  nofulllem3  25572  ontgval  26085  mblfinlem  26143  comppfsc  26277  neibastop2lem  26279  fnemeet2  26286  fnejoin1  26287  sstotbnd2  26373  heiborlem1  26410  heiborlem8  26417  intidl  26529  elrfi  26638  ismrcd1  26642  istopclsd  26644  mrefg2  26651  aomclem2  27020  aomclem6  27024  hbtlem6  27201  hbt  27202  symggen  27279  stoweidlem59  27675  bnj906  29007  bnj1020  29040  bnj1137  29070  bnj1408  29111  bnj1452  29127  lsmsat  29491  lssats  29495  lpssat  29496  lssatle  29498  lssat  29499  lsatcvatlem  29532  paddss12  30301  paddasslem17  30318  pmodlem1  30328  pmod1i  30330  pmodl42N  30333  elpcliN  30375  pclfinN  30382  polcon3N  30399  polcon2N  30401  paddunN  30409  pclfinclN  30432  poml5N  30436  osumcllem1N  30438  osumcllem2N  30439  osumcllem3N  30440  pl42lem2N  30462  pl42lem4N  30464  cdlemn5pre  31683  dihord1  31701  dihord2a  31702  dihord2b  31703  dihord5b  31742  dochss  31848  dochdmj1  31873  djhsumss  31890  djhunssN  31892  dochexmidlem2  31944  lclkrslem1  32020  lclkrslem2  32021  lcfrlem2  32026
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator