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

Theorem sstrd 3976
Description: Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)
Hypotheses
Ref Expression
sstrd.1 (𝜑𝐴𝐵)
sstrd.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
sstrd (𝜑𝐴𝐶)

Proof of Theorem sstrd
StepHypRef Expression
1 sstrd.1 . 2 (𝜑𝐴𝐵)
2 sstrd.2 . 2 (𝜑𝐵𝐶)
3 sstr 3974 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
41, 2, 3syl2anc 584 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951
This theorem is referenced by:  sstrid  3977  sstrdi  3978  rabssrabd  4057  ssdif2d  4119  uniintsn  4906  funss  6368  fssxp  6528  knatar  7099  tfisi  7561  suppssov1  7853  suppssfv  7857  tposss  7884  tfrlem1  8003  omwordri  8188  oewordri  8208  oeeui  8218  oaabs2  8262  omopthlem1  8272  ecinxp  8362  sbthlem1  8616  dffi2  8876  hartogslem1  8995  cantnfcl  9119  cantnflt  9124  cantnfp1lem3  9132  cantnflem3  9143  cnfcom  9152  cnfcom3lem  9155  rankssb  9266  tskwe  9368  dfac12lem2  9559  dfac12lem3  9560  cfflb  9670  cfcof  9685  ssfin2  9731  hsmexlem4  9840  ttukeylem6  9925  ttukeylem7  9926  fpwwe2lem1  10042  fpwwe2lem8  10048  fpwwe2lem11  10051  fpwwe2lem12  10052  canthnumlem  10059  canthwelem  10061  canthwe  10062  canthp1lem2  10064  pwfseqlem5  10074  wunex2  10149  tsktrss  10172  inttsk  10185  uzwo3  12332  supicc  12876  supiccub  12877  supicclub  12878  ssfzunsnext  12942  seqsplit  13393  seqf1olem2a  13398  seqz  13408  swrdval2  13998  trrelssd  14323  rtrclreclem4  14410  sumss  15071  qshash  15172  incexc  15182  incexc2  15183  prodss  15291  rpnnen2lem11  15567  vdwlem1  16307  ramub1lem1  16352  imasaddvallem  16792  imasvscaf  16802  mrerintcl  16858  ismred2  16864  mremre  16865  mrcuni  16882  mressmrcd  16888  submrc  16889  mrissmrid  16902  mreexexlem2d  16906  isacs2  16914  isacs1i  16918  invss  17021  ssctr  17085  funcres2b  17157  isacs3lem  17766  acsfiindd  17777  acsmapd  17778  acsmap2d  17779  tsrdir  17838  subsubm  17971  gsumwspan  18001  subsubg  18242  subgint  18243  cntzidss  18408  symggen  18529  pmtrdifellem1  18535  pmtrdifellem2  18536  pgpssslw  18670  lsmless1x  18700  lsmless2x  18701  lsmless12  18718  subglsm  18730  gsumval3lem2  18957  gsumzaddlem  18972  gsumzadd  18973  gsum2d  19023  dmdprdd  19052  dprdfeq0  19075  dprdspan  19080  dprdres  19081  dprdss  19082  dprdz  19083  subgdmdprd  19087  subgdprd  19088  dprdsn  19089  dprd2dlem1  19094  dprd2da  19095  dmdprdsplit2lem  19098  dprdsplit  19101  pgpfac1lem2  19128  pgpfac1lem3  19130  pgpfac1lem5  19132  subsubrg  19492  subdrgint  19513  lspss  19687  lspun  19690  lsslsp  19718  lmhmlsp  19752  lsmelval2  19788  lsmssspx  19791  lsppratlem2  19851  lsppratlem3  19852  lsppratlem4  19853  lbsextlem2  19862  lbsextlem3  19863  aspss  20036  mhpaddcl  20268  mhpvscacl  20271  ocvlsp  20750  cssmre  20767  obselocv  20802  obslbs  20804  toponmre  21631  neiint  21642  neiss  21647  lpss  21680  lpss3  21682  restopnb  21713  restfpw  21717  neitr  21718  restcls  21719  restntr  21720  restlp  21721  ordtbas  21730  pnfnei  21758  mnfnei  21759  iscnp4  21801  cnclsi  21810  isreg2  21915  discmp  21936  cmpcld  21940  uncmp  21941  sscmp  21943  hauscmplem  21944  cmpfi  21946  iunconnlem  21965  clsconn  21968  2ndcctbss  21993  restnlly  22020  llyrest  22023  nllyrest  22024  llyidm  22026  nllyidm  22027  cldllycmp  22033  dislly  22035  comppfsc  22070  llycmpkgen2  22088  ptbasfi  22119  txnlly  22175  txcmplem1  22179  tx1stc  22188  xkococnlem  22197  qtopval2  22234  basqtop  22249  tgqtop  22250  qtoprest  22255  kqreglem1  22279  kqreglem2  22280  kqnrmlem1  22281  kqnrmlem2  22282  fsubbas  22405  fgabs  22417  fbasrn  22422  trfil2  22425  trfg  22429  isufil2  22446  trufil  22448  ssufl  22456  ufileu  22457  filufint  22458  fmfnfmlem4  22495  fmfnfm  22496  flimss2  22510  flimss1  22511  fclsfnflim  22565  flimfnfcls  22566  fclscmp  22568  cnpfcfi  22578  alexsubALT  22589  clssubg  22646  clsnsg  22647  tsmsres  22681  ustexsym  22753  ustex2sym  22754  ustex3sym  22755  ustneism  22761  trust  22767  utoptop  22772  restutopopn  22776  utop2nei  22788  utopreg  22790  cfiluweak  22833  neipcfilu  22834  blssps  22963  blss  22964  blcld  23044  blsscls  23046  met1stc  23060  met2ndci  23061  metust  23097  cfilucfil  23098  restmetu  23109  tgqioo  23337  xrsblre  23348  reconnlem2  23364  xrge0gsumle  23370  xrge0tsms  23371  rescncf  23434  cnmpopc  23461  cnheibor  23488  cnllycmp  23489  lebnum  23497  phtpycn  23516  cfilfcls  23806  iscmet3lem2  23824  cmetss  23848  cncmet  23854  bcthlem4  23859  bcth3  23863  rrxcph  23924  rrxmetlem  23939  minveclem4a  23962  minveclem4  23964  ivthicc  23988  ovollb  24009  ovollb2lem  24018  ovollb2  24019  nulmbl2  24066  ioorcl2  24102  uniioombllem3  24115  uniioombllem4  24116  uniioombllem5  24117  opnmbllem  24131  volcn  24136  volivth  24137  mbfeqalem1  24171  itg10a  24240  mbfi1fseqlem4  24248  ditgcl  24385  ditgswap  24386  ditgsplitlem  24387  limcflf  24408  limcres  24413  dvbss  24428  dvbsss  24429  perfdvf  24430  dvreslem  24436  dvres2lem  24437  dvres3  24440  dvcnp  24445  dvcnp2  24446  dvcn  24447  dvnff  24449  dvn2bss  24456  dvnres  24457  cpnord  24461  dvaddbr  24464  dvmulbr  24465  dvcobr  24472  dvnfre  24478  dvmptres2  24488  dvmptntr  24497  dvcnvlem  24502  dvcnv  24503  dvferm1lem  24510  dvferm2lem  24512  dvlip  24519  dvlipcn  24520  dvlip2  24521  c1liplem1  24522  dvgt0lem1  24528  lhop1lem  24539  lhop  24542  dvcnvrelem1  24543  dvcnvrelem2  24544  dvcnvre  24545  dvfsumle  24547  dvfsumge  24548  dvfsumabs  24549  ftc1lem1  24561  ftc1lem2  24562  ftc1a  24563  ftc1lem4  24565  ftc2ditglem  24571  itgsubstlem  24574  ig1peu  24694  ig1pdvds  24699  taylfvallem1  24874  tayl0  24879  taylply2  24885  taylply  24886  dvtaylp  24887  dvntaylp  24888  dvntaylp0  24889  taylthlem1  24890  ulmdvlem1  24917  ulmdvlem3  24919  psercn  24943  pserdvlem2  24945  abelth  24958  xrlimcnp  25474  lgamucov  25543  wilthlem2  25574  sqff1o  25687  chtublem  25715  pntlemq  26105  pntlemf  26109  tglineintmo  26356  ttgcontlem1  26599  pthdlem1  27475  shintcli  29034  shub1  29087  mdslmd1lem1  30030  mdexchi  30040  chirredlem1  30095  mdsymlem5  30112  sumdmdii  30120  sumdmdlem2  30124  fnpreimac  30345  xrsupssd  30410  xrge0infssd  30412  swrdrn3  30557  swrdf1  30558  swrdrndisj  30559  xrge0tsmsd  30620  linds2eq  30869  lbsdiflsp0  30922  dimkerim  30923  fedgmullem1  30925  fedgmullem2  30926  fedgmul  30927  smatrcl  30961  locfinreflem  31004  cmpcref  31014  pnfneige0  31094  esum2d  31252  insiga  31296  sssigagen2  31305  dynkin  31326  dya2iocnei  31440  omsmon  31456  carsgclctunlem1  31475  carsggect  31476  omsmeas  31481  ftc2re  31769  fdvneggt  31771  fdvnegge  31773  reprsuc  31786  reprss  31788  reprlt  31790  reprinfz1  31793  logdivsqrle  31821  hgt750lemb  31827  bnj906  32102  bnj1020  32135  bnj1137  32165  bnj1408  32206  bnj1452  32222  erdszelem7  32342  erdszelem8  32343  erdsze2lem1  32348  connpconn  32380  cvmliftmolem1  32426  cvmlift2lem1  32447  cvmlift2lem9  32456  cvmlift2lem10  32457  cvmlift3lem6  32469  cvmlift3lem7  32470  satfsschain  32509  ss2mcls  32713  dftrpred3g  32970  frrlem8  33028  sssslt1  33158  sssslt2  33159  scutbdaybnd  33173  neibastop2lem  33606  fnemeet2  33613  fnejoin1  33614  ontgval  33677  unbdqndv1  33745  opnmbllem0  34810  ftc1anclem7  34855  ftc1anclem8  34856  ftc1anc  34857  sstotbnd2  34935  heiborlem1  34972  heiborlem8  34979  intidl  35190  lsmsat  36026  lssats  36030  lpssat  36031  lssatle  36033  lssat  36034  lsatcvatlem  36067  paddss12  36837  paddasslem17  36854  pmodlem1  36864  pmod1i  36866  pmodl42N  36869  elpcliN  36911  pclfinN  36918  polcon3N  36935  polcon2N  36937  paddunN  36945  pclfinclN  36968  poml5N  36972  osumcllem1N  36974  osumcllem2N  36975  osumcllem3N  36976  pl42lem2N  36998  pl42lem4N  37000  cdlemn5pre  38218  dihord1  38236  dihord2a  38237  dihord2b  38238  dihord5b  38277  dochss  38383  dochdmj1  38408  djhsumss  38425  djhunssN  38427  dochexmidlem2  38479  lclkrslem1  38555  lclkrslem2  38556  lcfrlem2  38561  elrfi  39171  ismrcd1  39175  istopclsd  39177  mrefg2  39184  aomclem2  39535  aomclem6  39539  hbtlem6  39609  hbt  39610  mptrcllem  39853  dfrcl2  39899  relexp0a  39941  trclimalb2  39951  frege81d  39972  k0004ss2  40382  imo72b2lem0  40396  imo72b2lem2  40398  imo72b2lem1  40402  imo72b2  40406  uzwo4  41195  ssin0  41197  ixpssmapc  41216  ssinc  41233  ssdec  41234  supxrre3  41473  uzfissfz  41474  ssuzfz  41497  supminfxr  41620  inficc  41690  ressiocsup  41710  ressioosup  41711  ressiooinf  41713  limccog  41781  limclner  41812  limsuppnfdlem  41862  limsupres  41866  limsupresuz2  41870  limsupequzlem  41883  limsupvaluz2  41899  supcnvlimsup  41901  limsupgtlem  41938  liminfresuz2  41948  cncfmptssg  42033  cncfuni  42049  icccncfext  42050  dvresntr  42082  dvmptresicc  42084  dvbdfbdioolem1  42093  dvdmsscn  42101  dvnxpaek  42107  dvnprodlem2  42112  stoweidlem59  42225  fourierdlem20  42293  fourierdlem42  42315  fourierdlem48  42320  fourierdlem49  42321  fourierdlem52  42324  fourierdlem58  42330  fourierdlem64  42336  fourierdlem73  42345  fourierdlem76  42348  fourierdlem80  42352  fourierdlem84  42356  fourierdlem93  42365  fourierdlem103  42375  fourierdlem104  42376  fourierdlem113  42385  etransclem18  42418  ioorrnopnlem  42470  salincl  42489  intsal  42494  fsumlesge0  42540  sge0cl  42544  sge0supre  42552  sge0less  42555  sge0split  42572  sge0seq  42609  caragensspw  42672  omessre  42673  caragendifcl  42677  caratheodorylem1  42689  0ome  42692  omess0  42697  caragencmpl  42698  hoicvr  42711  hoissrrn  42712  hoicvrrex  42719  ovnlecvr  42721  ovnsslelem  42723  ovnssle  42724  ovnsubaddlem1  42733  hoissrrn2  42741  hoidmv1lelem1  42754  hoidmvlelem1  42758  hoidmvlelem2  42759  hoidmvlelem4  42761  ovnlecvr2  42773  voncmpl  42784  hspmbl  42792  opnvonmbllem1  42795  ovolval5lem2  42816  ovolval5lem3  42817  vonioolem1  42843  pimdecfgtioc  42874  pimincfltioc  42875  pimdecfgtioo  42876  pimincfltioo  42877  issmflem  42885  cnfsmf  42898  incsmflem  42899  smfsssmf  42901  smfadd  42922  decsmflem  42923  smflim  42934  smfres  42946  smfmul  42951  smfpimbor1lem1  42954  smfco  42958  smfsuplem1  42966  smfsuplem3  42968  smflimsuplem1  42975  smflimsuplem4  42978  smflimsuplem7  42981  subsubmgm  43911  setrecsss  44701  elpglem1  44711
  Copyright terms: Public domain W3C validator