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

Theorem sstrd 3202
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 3200 . 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 3165
This theorem is referenced by:  syl5ss  3203  syl6ss  3204  ssdif2d  3328  uniintsn  3915  tfisi  4665  funss  5289  fssxp  5416  knatar  5873  suppssfv  6090  suppssov1  6091  tposss  6251  omwordri  6586  oewordri  6606  oeeui  6616  oaabs2  6659  omopthlem1  6669  ecinxp  6750  sbthlem1  6987  dffi2  7192  hartogslem1  7273  cantnfcl  7384  cantnflt  7389  cantnfp1lem3  7398  cantnflem3  7409  cnfcom  7419  cnfcom3lem  7422  rankssb  7536  tskwe  7599  dfac12lem2  7786  dfac12lem3  7787  cfflb  7901  cfcof  7916  ssfin2  7962  hsmexlem4  8071  ttukeylem6  8157  ttukeylem7  8158  fpwwe2lem1  8269  fpwwe2lem8  8275  fpwwe2lem11  8278  fpwwe2lem12  8279  canthnumlem  8286  canthwelem  8288  canthwe  8289  canthp1lem2  8291  pwfseqlem5  8301  wunex2  8376  tsktrss  8399  inttsk  8412  uzwo3  10327  seqsplit  11095  seqf1olem2a  11100  seqz  11110  swrdval2  11469  sumss  12213  qshash  12301  incexc  12312  incexc2  12313  rpnnen2lem11  12519  vdwlem1  13044  ramub1lem1  13089  imasaddvallem  13447  imasvscaf  13457  mrerintcl  13515  ismred2  13521  mremre  13522  mrcuni  13539  mressmrcd  13545  submrc  13546  mrissmrid  13559  mreexexlem2d  13563  isacs2  13571  isacs1i  13575  invss  13679  ssctr  13718  funcres2b  13787  isacs3lem  14285  acsfiindd  14296  acsmapd  14297  acsmap2d  14298  tsrdir  14376  subsubm  14450  gsumwspan  14484  subsubg  14656  subgint  14657  cntzidss  14829  pgpssslw  14941  lsmless1x  14971  lsmless2x  14972  lsmless12  14988  subglsm  14998  gsumval3  15207  gsumzadd  15220  gsum2d  15239  dmdprdd  15253  dprdfeq0  15273  dprdspan  15278  dprdres  15279  dprdss  15280  dprdz  15281  subgdmdprd  15285  subgdprd  15286  dprdsn  15287  dprd2dlem1  15292  dprd2da  15293  dmdprdsplit2lem  15296  dprdsplit  15299  pgpfac1lem2  15326  pgpfac1lem3  15328  pgpfac1lem5  15330  subsubrg  15587  lspss  15757  lspun  15760  lsslsp  15788  lmhmlsp  15822  lsmelval2  15854  lsmssspx  15857  lsppratlem2  15917  lsppratlem3  15918  lsppratlem4  15919  lbsextlem2  15928  lbsextlem3  15929  aspss  16088  ocvlsp  16592  cssmre  16609  obselocv  16644  obslbs  16646  toponmre  16846  neiint  16857  neiss  16862  lpss  16890  lpss3  16892  restopnb  16922  restfpw  16926  restcls  16927  restntr  16928  restlp  16929  ordtbas  16938  pnfnei  16966  mnfnei  16967  cnclsi  17017  isreg2  17121  discmp  17141  cmpcld  17145  uncmp  17146  sscmp  17148  hauscmplem  17149  cmpfi  17151  iunconlem  17169  clscon  17172  2ndcctbss  17197  restnlly  17224  llyrest  17227  nllyrest  17228  llyidm  17230  nllyidm  17231  cldllycmp  17237  dislly  17239  llycmpkgen2  17261  ptbasfi  17292  txnlly  17347  txcmplem1  17351  tx1stc  17360  xkococnlem  17369  qtopval2  17403  basqtop  17418  tgqtop  17419  qtoprest  17424  kqreglem1  17448  kqreglem2  17449  kqnrmlem1  17450  kqnrmlem2  17451  fsubbas  17578  fgabs  17590  fbasrn  17595  trfil2  17598  trfg  17602  isufil2  17619  trufil  17621  ssufl  17629  ufileu  17630  filufint  17631  fmfnfmlem4  17668  fmfnfm  17669  flimss2  17683  flimss1  17684  fclsfnflim  17738  flimfnfcls  17739  fclscmp  17741  cnpfcfi  17751  alexsubALT  17761  clssubg  17807  clsnsg  17808  blss  17988  blcld  18067  blsscls  18069  met1stc  18083  met2ndci  18084  tgqioo  18322  xrsblre  18333  reconnlem2  18348  xrge0gsumle  18354  xrge0tsms  18355  rescncf  18417  cnmpt2pc  18442  cnheibor  18469  cnllycmp  18470  lebnum  18478  phtpycn  18497  cfilfcls  18716  iscmet3lem2  18734  cmetss  18756  cncmet  18760  bcthlem4  18765  bcth3  18769  minveclem4a  18810  minveclem4  18812  ivthicc  18834  ovollb  18854  ovollb2lem  18863  ovollb2  18864  nulmbl2  18910  ioorcl2  18943  uniioombllem3  18956  uniioombllem4  18957  uniioombllem5  18958  opnmbllem  18972  volcn  18977  volivth  18978  mbfeqalem  19013  itg10a  19081  mbfi1fseqlem4  19089  ditgcl  19224  ditgswap  19225  ditgsplitlem  19226  limcflf  19247  limcres  19252  dvbss  19267  dvbsss  19268  perfdvf  19269  dvreslem  19275  dvres2lem  19276  dvres3  19279  dvcnp  19284  dvcnp2  19285  dvcn  19286  dvnff  19288  dvn2bss  19295  dvnres  19296  cpnord  19300  dvaddbr  19303  dvmulbr  19304  dvaddf  19307  dvmulf  19308  dvcobr  19311  dvcof  19313  dvnfre  19317  dvmptres2  19327  dvmptntr  19336  dvcnvlem  19339  dvcnv  19340  dvferm1lem  19347  dvferm2lem  19349  dvlip  19356  dvlipcn  19357  dvlip2  19358  c1liplem1  19359  dvgt0lem1  19365  lhop1lem  19376  lhop  19379  dvcnvrelem1  19380  dvcnvrelem2  19381  dvcnvre  19382  dvfsumle  19384  dvfsumge  19385  dvfsumabs  19386  ftc1lem1  19398  ftc1lem2  19399  ftc1a  19400  ftc1lem4  19402  ftc2ditglem  19408  itgsubstlem  19411  ig1peu  19573  ig1pdvds  19578  taylfvallem1  19752  tayl0  19757  taylply2  19763  taylply  19764  dvtaylp  19765  dvntaylp  19766  dvntaylp0  19767  taylthlem1  19768  ulmdvlem1  19793  ulmdvlem3  19795  psercn  19818  pserdvlem2  19820  abelth  19833  xrlimcnp  20279  wilthlem2  20323  sqff1o  20436  chtublem  20466  pntlemq  20766  pntlemf  20770  ghsubgolem  21053  shintcli  21924  shub1  21977  mdslmd1lem1  22921  mdexchi  22931  chirredlem1  22986  mdsymlem5  23003  sumdmdii  23011  sumdmdlem2  23015  xrsupssd  23269  pnfneige0  23389  xrge0tsmsd  23397  sigaclci  23508  insiga  23513  sssigagen2  23522  erdszelem7  23743  erdszelem8  23744  erdsze2lem1  23749  conpcon  23781  cvmliftmolem1  23827  cvmlift2lem1  23848  cvmlift2lem9  23857  cvmlift2lem10  23858  cvmlift3lem6  23870  cvmlift3lem7  23871  rtrclreclem.min  24059  dftrpred3g  24307  nofulllem3  24429  ontgval  24942  efilcp  25655  iscnp4  25666  islimrs4  25685  comppfsc  26410  neibastop2lem  26412  fnemeet2  26419  fnejoin1  26420  sstotbnd2  26601  heiborlem1  26638  heiborlem8  26645  intidl  26757  elrfi  26872  ismrcd1  26876  istopclsd  26878  mrefg2  26885  aomclem2  27255  aomclem6  27259  hbtlem6  27436  hbt  27437  symggen  27514  stoweidlem34  27886  bnj906  29278  bnj1020  29311  bnj1137  29341  bnj1408  29382  bnj1452  29398  lsmsat  29820  lssats  29824  lpssat  29825  lssatle  29827  lssat  29828  lsatcvatlem  29861  paddss12  30630  paddasslem17  30647  pmodlem1  30657  pmod1i  30659  pmodl42N  30662  elpcliN  30704  pclfinN  30711  polcon3N  30728  polcon2N  30730  paddunN  30738  pclfinclN  30761  poml5N  30765  osumcllem1N  30767  osumcllem2N  30768  osumcllem3N  30769  pl42lem2N  30791  pl42lem4N  30793  cdlemn5pre  32012  dihord1  32030  dihord2a  32031  dihord2b  32032  dihord5b  32071  dochss  32177  dochdmj1  32202  djhsumss  32219  djhunssN  32221  dochexmidlem2  32273  lclkrslem1  32349  lclkrslem2  32350  lcfrlem2  32355
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator