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

Theorem sstrd 3577
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 3575 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
41, 2, 3syl2anc 690 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  syl5ss  3578  syl6ss  3579  ssdif2d  3710  uniintsn  4443  funss  5808  fssxp  5959  fimass  5979  knatar  6485  tfisi  6927  suppfnss  7184  suppssov1  7191  suppssfv  7195  tposss  7217  tfrlem1  7336  omwordri  7516  oewordri  7536  oeeui  7546  oaabs2  7589  omopthlem1  7599  ecinxp  7686  sbthlem1  7932  dffi2  8189  hartogslem1  8307  cantnfcl  8424  cantnflt  8429  cantnfp1lem3  8437  cantnflem3  8448  cnfcom  8457  cnfcom3lem  8460  rankssb  8571  tskwe  8636  dfac12lem2  8826  dfac12lem3  8827  cfflb  8941  cfcof  8956  ssfin2  9002  hsmexlem4  9111  ttukeylem6  9196  ttukeylem7  9197  fpwwe2lem1  9309  fpwwe2lem8  9315  fpwwe2lem11  9318  fpwwe2lem12  9319  canthnumlem  9326  canthwelem  9328  canthwe  9329  canthp1lem2  9331  pwfseqlem5  9341  wunex2  9416  tsktrss  9439  inttsk  9452  uzwo3  11615  supicc  12147  supiccub  12148  supicclub  12149  ssfzunsn  12212  seqsplit  12651  seqf1olem2a  12656  seqz  12666  swrdval2  13218  trrelssd  13506  rtrclreclem4  13595  sumss  14248  qshash  14344  incexc  14354  incexc2  14355  prodss  14462  rpnnen2lem11  14738  vdwlem1  15469  ramub1lem1  15514  imasaddvallem  15958  imasvscaf  15968  mrerintcl  16026  ismred2  16032  mremre  16033  mrcuni  16050  mressmrcd  16056  submrc  16057  mrissmrid  16070  mreexexlem2d  16074  isacs2  16083  isacs1i  16087  invss  16190  ssctr  16254  funcres2b  16326  isacs3lem  16935  acsfiindd  16946  acsmapd  16947  acsmap2d  16948  tsrdir  17007  subsubm  17126  gsumwspan  17152  subsubg  17386  subgint  17387  cntzidss  17539  symggen  17659  pmtrdifellem1  17665  pmtrdifellem2  17666  pgpssslw  17798  lsmless1x  17828  lsmless2x  17829  lsmless12  17845  subglsm  17855  gsumval3lem2  18076  gsumzaddlem  18090  gsumzadd  18091  gsum2d  18140  dmdprdd  18167  dprdfeq0  18190  dprdspan  18195  dprdres  18196  dprdss  18197  dprdz  18198  subgdmdprd  18202  subgdprd  18203  dprdsn  18204  dprd2dlem1  18209  dprd2da  18210  dmdprdsplit2lem  18213  dprdsplit  18216  pgpfac1lem2  18243  pgpfac1lem3  18245  pgpfac1lem5  18247  subsubrg  18575  lspss  18751  lspun  18754  lsslsp  18782  lmhmlsp  18816  lsmelval2  18852  lsmssspx  18855  lsppratlem2  18915  lsppratlem3  18916  lsppratlem4  18917  lbsextlem2  18926  lbsextlem3  18927  aspss  19099  ocvlsp  19781  cssmre  19798  obselocv  19833  obslbs  19835  toponmre  20649  neiint  20660  neiss  20665  lpss  20698  lpss3  20700  restopnb  20731  restfpw  20735  neitr  20736  restcls  20737  restntr  20738  restlp  20739  ordtbas  20748  pnfnei  20776  mnfnei  20777  iscnp4  20819  cnclsi  20828  isreg2  20933  discmp  20953  cmpcld  20957  uncmp  20958  sscmp  20960  hauscmplem  20961  cmpfi  20963  iunconlem  20982  clscon  20985  2ndcctbss  21010  restnlly  21037  llyrest  21040  nllyrest  21041  llyidm  21043  nllyidm  21044  cldllycmp  21050  dislly  21052  comppfsc  21087  llycmpkgen2  21105  ptbasfi  21136  txnlly  21192  txcmplem1  21196  tx1stc  21205  xkococnlem  21214  qtopval2  21251  basqtop  21266  tgqtop  21267  qtoprest  21272  kqreglem1  21296  kqreglem2  21297  kqnrmlem1  21298  kqnrmlem2  21299  fsubbas  21423  fgabs  21435  fbasrn  21440  trfil2  21443  trfg  21447  isufil2  21464  trufil  21466  ssufl  21474  ufileu  21475  filufint  21476  fmfnfmlem4  21513  fmfnfm  21514  flimss2  21528  flimss1  21529  fclsfnflim  21583  flimfnfcls  21584  fclscmp  21586  cnpfcfi  21596  alexsubALT  21607  clssubg  21664  clsnsg  21665  tsmsres  21699  ustexsym  21771  ustex2sym  21772  ustex3sym  21773  ustund  21777  ustneism  21779  trust  21785  utoptop  21790  restutopopn  21794  utop2nei  21806  utopreg  21808  cfiluweak  21851  neipcfilu  21852  blssps  21980  blss  21981  blcld  22061  blsscls  22063  met1stc  22077  met2ndci  22078  metust  22114  cfilucfil  22115  restmetu  22126  tgqioo  22343  xrsblre  22354  reconnlem2  22370  xrge0gsumle  22376  xrge0tsms  22377  rescncf  22439  cnmpt2pc  22466  cnheibor  22493  cnllycmp  22494  lebnum  22502  phtpycn  22521  cfilfcls  22798  iscmet3lem2  22816  cmetss  22838  cncmet  22844  bcthlem4  22849  bcth3  22853  rrxcph  22905  rrxmetlem  22915  minveclem4a  22926  minveclem4  22928  ivthicc  22951  ovollb  22971  ovollb2lem  22980  ovollb2  22981  nulmbl2  23028  ioorcl2  23063  uniioombllem3  23076  uniioombllem4  23077  uniioombllem5  23078  opnmbllem  23092  volcn  23097  volivth  23098  mbfeqalem  23132  itg10a  23200  mbfi1fseqlem4  23208  ditgcl  23345  ditgswap  23346  ditgsplitlem  23347  limcflf  23368  limcres  23373  dvbss  23388  dvbsss  23389  perfdvf  23390  dvreslem  23396  dvres2lem  23397  dvres3  23400  dvcnp  23405  dvcnp2  23406  dvcn  23407  dvnff  23409  dvn2bss  23416  dvnres  23417  cpnord  23421  dvaddbr  23424  dvmulbr  23425  dvcobr  23432  dvnfre  23438  dvmptres2  23448  dvmptntr  23457  dvcnvlem  23460  dvcnv  23461  dvferm1lem  23468  dvferm2lem  23470  dvlip  23477  dvlipcn  23478  dvlip2  23479  c1liplem1  23480  dvgt0lem1  23486  lhop1lem  23497  lhop  23500  dvcnvrelem1  23501  dvcnvrelem2  23502  dvcnvre  23503  dvfsumle  23505  dvfsumge  23506  dvfsumabs  23507  ftc1lem1  23519  ftc1lem2  23520  ftc1a  23521  ftc1lem4  23523  ftc2ditglem  23529  itgsubstlem  23532  ig1peu  23652  ig1pdvds  23657  taylfvallem1  23832  tayl0  23837  taylply2  23843  taylply  23844  dvtaylp  23845  dvntaylp  23846  dvntaylp0  23847  taylthlem1  23848  ulmdvlem1  23875  ulmdvlem3  23877  psercn  23901  pserdvlem2  23903  abelth  23916  xrlimcnp  24412  lgamucov  24481  wilthlem2  24512  sqff1o  24625  chtublem  24653  pntlemq  25007  pntlemf  25011  tglineintmo  25255  ttgcontlem1  25483  shintcli  27378  shub1  27431  mdslmd1lem1  28374  mdexchi  28384  chirredlem1  28439  mdsymlem5  28456  sumdmdii  28464  sumdmdlem2  28468  xrsupssd  28720  xrge0infssd  28722  xrge0tsmsd  28922  smatrcl  28996  locfinreflem  29041  cmpcref  29051  pnfneige0  29131  esum2d  29288  insiga  29333  sssigagen2  29342  dynkin  29363  dya2iocnei  29477  omsmon  29493  carsgclctunlem1  29512  carsggect  29513  omsmeas  29518  bnj906  30060  bnj1020  30093  bnj1137  30123  bnj1408  30164  bnj1452  30180  erdszelem7  30239  erdszelem8  30240  erdsze2lem1  30245  conpcon  30277  cvmliftmolem1  30323  cvmlift2lem1  30344  cvmlift2lem9  30353  cvmlift2lem10  30354  cvmlift3lem6  30366  cvmlift3lem7  30367  ss2mcls  30525  dftrpred3g  30783  nofulllem3  30909  neibastop2lem  31331  fnemeet2  31338  fnejoin1  31339  ontgval  31406  unbdqndv1  31475  opnmbllem0  32411  ftc1anclem7  32457  ftc1anclem8  32458  ftc1anc  32459  sstotbnd2  32539  heiborlem1  32576  heiborlem8  32583  intidl  32794  lsmsat  33109  lssats  33113  lpssat  33114  lssatle  33116  lssat  33117  lsatcvatlem  33150  paddss12  33919  paddasslem17  33936  pmodlem1  33946  pmod1i  33948  pmodl42N  33951  elpcliN  33993  pclfinN  34000  polcon3N  34017  polcon2N  34019  paddunN  34027  pclfinclN  34050  poml5N  34054  osumcllem1N  34056  osumcllem2N  34057  osumcllem3N  34058  pl42lem2N  34080  pl42lem4N  34082  cdlemn5pre  35303  dihord1  35321  dihord2a  35322  dihord2b  35323  dihord5b  35362  dochss  35468  dochdmj1  35493  djhsumss  35510  djhunssN  35512  dochexmidlem2  35564  lclkrslem1  35640  lclkrslem2  35641  lcfrlem2  35646  elrfi  36071  ismrcd1  36075  istopclsd  36077  mrefg2  36084  aomclem2  36439  aomclem6  36443  hbtlem6  36514  hbt  36515  mptrcllem  36735  dfrcl2  36781  relexp0a  36823  trclimalb2  36833  frege81d  36854  k0004ss2  37266  imo72b2lem0  37283  imo72b2lem2  37285  imo72b2lem1  37289  imo72b2  37293  uzwo4  38042  ssin0  38044  ixpssmapc  38065  ssinc  38088  ssdec  38089  supxrre3  38279  uzfissfz  38280  ssuzfz  38303  inficc  38405  ressiocsup  38425  ressioosup  38426  ressiooinf  38428  limccog  38484  limclner  38515  cncfmptssg  38552  cncfuni  38569  icccncfext  38570  dvresntr  38603  dvmptresicc  38606  dvbdfbdioolem1  38615  dvdmsscn  38623  dvnxpaek  38629  dvnprodlem2  38634  stoweidlem59  38749  fourierdlem20  38817  fourierdlem42  38839  fourierdlem48  38844  fourierdlem49  38845  fourierdlem52  38848  fourierdlem58  38854  fourierdlem64  38860  fourierdlem73  38869  fourierdlem76  38872  fourierdlem80  38876  fourierdlem84  38880  fourierdlem93  38889  fourierdlem103  38899  fourierdlem104  38900  fourierdlem113  38909  etransclem18  38942  ioorrnopnlem  38997  salincl  39016  intsal  39021  fsumlesge0  39067  sge0cl  39071  sge0supre  39079  sge0less  39082  sge0split  39099  sge0seq  39136  caragensspw  39196  omessre  39197  caragendifcl  39201  caratheodorylem1  39213  0ome  39216  omess0  39221  caragencmpl  39222  hoicvr  39235  hoissrrn  39236  hoicvrrex  39243  ovnlecvr  39245  ovnsslelem  39247  ovnssle  39248  ovnsubaddlem1  39257  hoissrrn2  39265  hoidmv1lelem1  39278  hoidmvlelem1  39282  hoidmvlelem2  39283  hoidmvlelem4  39285  ovnlecvr2  39297  voncmpl  39308  hspmbl  39316  opnvonmbllem1  39319  ovolval5lem2  39340  ovolval5lem3  39341  vonioolem1  39368  pimdecfgtioc  39399  pimincfltioc  39400  pimdecfgtioo  39401  pimincfltioo  39402  issmflem  39410  cnfsmf  39424  incsmflem  39425  smfsssmf  39427  smfadd  39448  decsmflem  39449  smflim  39460  smfres  39472  smfmul  39477  smfpimbor1lem1  39480  smfco  39484  pthdlem1  40967  subsubmgm  41582
  Copyright terms: Public domain W3C validator