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

Theorem sstrd 3474
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 3472 . 2  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
41, 2, 3syl2anc 665 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450
This theorem is referenced by:  syl5ss  3475  syl6ss  3476  ssdif2d  3604  uniintsn  4293  funss  5619  fssxp  5758  knatar  6263  tfisi  6699  suppfnss  6951  suppssov1  6958  suppssfv  6962  tposss  6985  tfrlem1  7105  omwordri  7284  oewordri  7304  oeeui  7314  oaabs2  7357  omopthlem1  7367  ecinxp  7449  sbthlem1  7691  dffi2  7946  hartogslem1  8066  cantnfcl  8180  cantnflt  8185  cantnfp1lem3  8193  cantnflem3  8204  cnfcom  8213  cnfcom3lem  8216  rankssb  8327  tskwe  8392  dfac12lem2  8581  dfac12lem3  8582  cfflb  8696  cfcof  8711  ssfin2  8757  hsmexlem4  8866  ttukeylem6  8951  ttukeylem7  8952  fpwwe2lem1  9063  fpwwe2lem8  9069  fpwwe2lem11  9072  fpwwe2lem12  9073  canthnumlem  9080  canthwelem  9082  canthwe  9083  canthp1lem2  9085  pwfseqlem5  9095  wunex2  9170  tsktrss  9193  inttsk  9206  uzwo3  11266  supicc  11787  supiccub  11788  supicclub  11789  seqsplit  12252  seqf1olem2a  12257  seqz  12267  swrdval2  12778  trrelssd  13037  rtrclreclem4  13124  sumss  13789  qshash  13884  incexc  13894  incexc2  13895  prodss  14000  rpnnen2lem11  14276  vdwlem1  14930  ramub1lem1  14983  imasaddvallem  15434  imasvscaf  15444  mrerintcl  15502  ismred2  15508  mremre  15509  mrcuni  15526  mressmrcd  15532  submrc  15533  mrissmrid  15546  mreexexlem2d  15550  isacs2  15558  isacs1i  15562  invss  15665  ssctr  15729  funcres2b  15801  isacs3lem  16411  acsfiindd  16422  acsmapd  16423  acsmap2d  16424  tsrdir  16483  subsubm  16603  gsumwspan  16629  subsubg  16839  subgint  16840  cntzidss  16990  symggen  17110  pmtrdifellem1  17116  pmtrdifellem2  17117  pgpssslw  17265  lsmless1x  17295  lsmless2x  17296  lsmless12  17312  subglsm  17322  gsumval3lem2  17539  gsumzaddlem  17553  gsumzadd  17554  gsum2d  17603  dmdprdd  17630  dprdfeq0  17654  dprdspan  17659  dprdres  17660  dprdss  17661  dprdz  17662  subgdmdprd  17666  subgdprd  17667  dprdsn  17668  dprd2dlem1  17673  dprd2da  17674  dmdprdsplit2lem  17677  dprdsplit  17680  pgpfac1lem2  17707  pgpfac1lem3  17709  pgpfac1lem5  17711  subsubrg  18033  lspss  18206  lspun  18209  lsslsp  18237  lmhmlsp  18271  lsmelval2  18307  lsmssspx  18310  lsppratlem2  18370  lsppratlem3  18371  lsppratlem4  18372  lbsextlem2  18381  lbsextlem3  18382  aspss  18555  ocvlsp  19237  cssmre  19254  obselocv  19289  obslbs  19291  toponmre  20107  neiint  20118  neiss  20123  lpss  20156  lpss3  20158  restopnb  20189  restfpw  20193  neitr  20194  restcls  20195  restntr  20196  restlp  20197  ordtbas  20206  pnfnei  20234  mnfnei  20235  iscnp4  20277  cnclsi  20286  isreg2  20391  discmp  20411  cmpcld  20415  uncmp  20416  sscmp  20418  hauscmplem  20419  cmpfi  20421  iunconlem  20440  clscon  20443  2ndcctbss  20468  restnlly  20495  llyrest  20498  nllyrest  20499  llyidm  20501  nllyidm  20502  cldllycmp  20508  dislly  20510  comppfsc  20545  llycmpkgen2  20563  ptbasfi  20594  txnlly  20650  txcmplem1  20654  tx1stc  20663  xkococnlem  20672  qtopval2  20709  basqtop  20724  tgqtop  20725  qtoprest  20730  kqreglem1  20754  kqreglem2  20755  kqnrmlem1  20756  kqnrmlem2  20757  fsubbas  20880  fgabs  20892  fbasrn  20897  trfil2  20900  trfg  20904  isufil2  20921  trufil  20923  ssufl  20931  ufileu  20932  filufint  20933  fmfnfmlem4  20970  fmfnfm  20971  flimss2  20985  flimss1  20986  fclsfnflim  21040  flimfnfcls  21041  fclscmp  21043  cnpfcfi  21053  alexsubALT  21064  clssubg  21121  clsnsg  21122  tsmsres  21156  ustexsym  21228  ustex2sym  21229  ustex3sym  21230  ustund  21234  ustneism  21236  trust  21242  utoptop  21247  restutopopn  21251  utop2nei  21263  utopreg  21265  cfiluweak  21308  neipcfilu  21309  blssps  21437  blss  21438  blcld  21518  blsscls  21520  met1stc  21534  met2ndci  21535  metust  21571  cfilucfil  21572  restmetu  21583  tgqioo  21816  xrsblre  21827  reconnlem2  21843  xrge0gsumle  21849  xrge0tsms  21850  rescncf  21927  cnmpt2pc  21954  cnheibor  21981  cnllycmp  21982  lebnum  21993  phtpycn  22012  cfilfcls  22242  iscmet3lem2  22260  cmetss  22282  cncmet  22288  bcthlem4  22293  bcth3  22297  rrxcph  22349  rrxmetlem  22359  minveclem4a  22370  minveclem4  22372  minveclem4aOLD  22382  minveclem4OLD  22384  ivthicc  22407  ovollb  22430  ovollb2lem  22439  ovollb2  22440  nulmbl2  22488  ioorcl2  22522  uniioombllem3  22541  uniioombllem4  22542  uniioombllem5  22543  opnmbllem  22557  volcn  22562  volivth  22563  mbfeqalem  22596  itg10a  22666  mbfi1fseqlem4  22674  ditgcl  22811  ditgswap  22812  ditgsplitlem  22813  limcflf  22834  limcres  22839  dvbss  22854  dvbsss  22855  perfdvf  22856  dvreslem  22862  dvres2lem  22863  dvres3  22866  dvcnp  22871  dvcnp2  22872  dvcn  22873  dvnff  22875  dvn2bss  22882  dvnres  22883  cpnord  22887  dvaddbr  22890  dvmulbr  22891  dvcobr  22898  dvnfre  22904  dvmptres2  22914  dvmptntr  22923  dvcnvlem  22926  dvcnv  22927  dvferm1lem  22934  dvferm2lem  22936  dvlip  22943  dvlipcn  22944  dvlip2  22945  c1liplem1  22946  dvgt0lem1  22952  lhop1lem  22963  lhop  22966  dvcnvrelem1  22967  dvcnvrelem2  22968  dvcnvre  22969  dvfsumle  22971  dvfsumge  22972  dvfsumabs  22973  ftc1lem1  22985  ftc1lem2  22986  ftc1a  22987  ftc1lem4  22989  ftc2ditglem  22995  itgsubstlem  22998  ig1peu  23120  ig1peuOLD  23121  ig1pdvds  23126  ig1pdvdsOLD  23132  taylfvallem1  23310  tayl0  23315  taylply2  23321  taylply  23322  dvtaylp  23323  dvntaylp  23324  dvntaylp0  23325  taylthlem1  23326  ulmdvlem1  23353  ulmdvlem3  23355  psercn  23379  pserdvlem2  23381  abelth  23394  xrlimcnp  23892  lgamucov  23961  wilthlem2  23992  sqff1o  24107  chtublem  24137  pntlemq  24437  pntlemf  24441  tglineintmo  24685  ttgcontlem1  24913  ghsubgolemOLD  26096  shintcli  26980  shub1  27033  mdslmd1lem1  27976  mdexchi  27986  chirredlem1  28041  mdsymlem5  28058  sumdmdii  28066  sumdmdlem2  28070  xrsupssd  28345  xrge0infssd  28348  xrge0infssdOLD  28349  xrge0tsmsd  28556  smatrcl  28630  locfinreflem  28675  cmpcref  28685  pnfneige0  28765  esum2d  28922  insiga  28967  sssigagen2  28976  dynkin  28997  dya2iocnei  29112  omsmon  29134  omsmonOLD  29138  carsgclctunlem1  29157  carsggect  29158  omsmeas  29163  omsmeasOLD  29164  bnj906  29749  bnj1020  29782  bnj1137  29812  bnj1408  29853  bnj1452  29869  erdszelem7  29928  erdszelem8  29929  erdsze2lem1  29934  conpcon  29966  cvmliftmolem1  30012  cvmlift2lem1  30033  cvmlift2lem9  30042  cvmlift2lem10  30043  cvmlift3lem6  30055  cvmlift3lem7  30056  ss2mcls  30214  dftrpred3g  30481  nofulllem3  30598  neibastop2lem  31021  fnemeet2  31028  fnejoin1  31029  ontgval  31096  opnmbllem0  31940  ftc1anclem7  31987  ftc1anclem8  31988  ftc1anc  31989  sstotbnd2  32070  heiborlem1  32107  heiborlem8  32114  intidl  32226  lsmsat  32543  lssats  32547  lpssat  32548  lssatle  32550  lssat  32551  lsatcvatlem  32584  paddss12  33353  paddasslem17  33370  pmodlem1  33380  pmod1i  33382  pmodl42N  33385  elpcliN  33427  pclfinN  33434  polcon3N  33451  polcon2N  33453  paddunN  33461  pclfinclN  33484  poml5N  33488  osumcllem1N  33490  osumcllem2N  33491  osumcllem3N  33492  pl42lem2N  33514  pl42lem4N  33516  cdlemn5pre  34737  dihord1  34755  dihord2a  34756  dihord2b  34757  dihord5b  34796  dochss  34902  dochdmj1  34927  djhsumss  34944  djhunssN  34946  dochexmidlem2  34998  lclkrslem1  35074  lclkrslem2  35075  lcfrlem2  35080  elrfi  35505  ismrcd1  35509  istopclsd  35511  mrefg2  35518  aomclem2  35883  aomclem6  35887  hbtlem6  35958  hbt  35959  mptrcllem  36190  dfrcl2  36236  relexp0a  36278  trclimalb2  36288  frege81d  36309  imo72b2lem0  36578  imo72b2lem2  36580  imo72b2lem1  36584  imo72b2  36589  uzwo4  37365  ssin0  37368  fimass  37403  supxrre3  37502  uzfissfz  37503  ssuzfz  37526  inficc  37584  limccog  37640  limclner  37672  cncfmptssg  37687  cncfuni  37704  icccncfext  37705  dvresntr  37728  dvmptresicc  37731  dvbdfbdioolem1  37740  dvdmsscn  37751  dvnxpaek  37757  dvnprodlem2  37762  stoweidlem59  37860  fourierdlem20  37929  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem48  37958  fourierdlem49  37959  fourierdlem52  37962  fourierdlem58  37968  fourierdlem64  37974  fourierdlem73  37983  fourierdlem76  37986  fourierdlem80  37990  fourierdlem84  37994  fourierdlem93  38003  fourierdlem103  38013  fourierdlem104  38014  fourierdlem113  38023  etransclem18  38057  salincl  38105  intsal  38110  fsumlesge0  38127  sge0cl  38131  sge0supre  38139  sge0less  38142  sge0split  38159  caragensspw  38238  omessre  38239  caragendifcl  38243  caratheodorylem1  38255  0ome  38258  hoicvr  38274  hoissrrn  38275  hoicvrrex  38282  ovnlecvr  38284  ovnsslelem  38286  ovnssle  38287  ovnsubaddlem1  38296  hoissrrn2  38304  hoidmv1lelem1  38317  hoidmvlelem1  38321  hoidmvlelem2  38322  hoidmvlelem4  38324  subsubmgm  39417
  Copyright terms: Public domain W3C validator