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

Theorem sstrd 3646
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 3644 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
41, 2, 3syl2anc 694 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  syl5ss  3647  syl6ss  3648  ssdif2d  3782  uniintsn  4546  funss  5945  fssxp  6098  fimass  6119  knatar  6647  tfisi  7100  suppfnss  7365  suppssov1  7372  suppssfv  7376  tposss  7398  tfrlem1  7517  omwordri  7697  oewordri  7717  oeeui  7727  oaabs2  7770  omopthlem1  7780  ecinxp  7865  sbthlem1  8111  dffi2  8370  hartogslem1  8488  cantnfcl  8602  cantnflt  8607  cantnfp1lem3  8615  cantnflem3  8626  cnfcom  8635  cnfcom3lem  8638  rankssb  8749  tskwe  8814  dfac12lem2  9004  dfac12lem3  9005  cfflb  9119  cfcof  9134  ssfin2  9180  hsmexlem4  9289  ttukeylem6  9374  ttukeylem7  9375  fpwwe2lem1  9491  fpwwe2lem8  9497  fpwwe2lem11  9500  fpwwe2lem12  9501  canthnumlem  9508  canthwelem  9510  canthwe  9511  canthp1lem2  9513  pwfseqlem5  9523  wunex2  9598  tsktrss  9621  inttsk  9634  uzwo3  11821  supicc  12358  supiccub  12359  supicclub  12360  ssfzunsnext  12424  seqsplit  12874  seqf1olem2a  12879  seqz  12889  swrdval2  13465  trrelssd  13758  rtrclreclem4  13845  sumss  14499  qshash  14603  incexc  14613  incexc2  14614  prodss  14721  rpnnen2lem11  14997  vdwlem1  15732  ramub1lem1  15777  imasaddvallem  16236  imasvscaf  16246  mrerintcl  16304  ismred2  16310  mremre  16311  mrcuni  16328  mressmrcd  16334  submrc  16335  mrissmrid  16348  mreexexlem2d  16352  isacs2  16361  isacs1i  16365  invss  16468  ssctr  16532  funcres2b  16604  isacs3lem  17213  acsfiindd  17224  acsmapd  17225  acsmap2d  17226  tsrdir  17285  subsubm  17404  gsumwspan  17430  subsubg  17664  subgint  17665  cntzidss  17816  symggen  17936  pmtrdifellem1  17942  pmtrdifellem2  17943  pgpssslw  18075  lsmless1x  18105  lsmless2x  18106  lsmless12  18122  subglsm  18132  gsumval3lem2  18353  gsumzaddlem  18367  gsumzadd  18368  gsum2d  18417  dmdprdd  18444  dprdfeq0  18467  dprdspan  18472  dprdres  18473  dprdss  18474  dprdz  18475  subgdmdprd  18479  subgdprd  18480  dprdsn  18481  dprd2dlem1  18486  dprd2da  18487  dmdprdsplit2lem  18490  dprdsplit  18493  pgpfac1lem2  18520  pgpfac1lem3  18522  pgpfac1lem5  18524  subsubrg  18854  lspss  19032  lspun  19035  lsslsp  19063  lmhmlsp  19097  lsmelval2  19133  lsmssspx  19136  lsppratlem2  19196  lsppratlem3  19197  lsppratlem4  19198  lbsextlem2  19207  lbsextlem3  19208  aspss  19380  ocvlsp  20068  cssmre  20085  obselocv  20120  obslbs  20122  toponmre  20945  neiint  20956  neiss  20961  lpss  20994  lpss3  20996  restopnb  21027  restfpw  21031  neitr  21032  restcls  21033  restntr  21034  restlp  21035  ordtbas  21044  pnfnei  21072  mnfnei  21073  iscnp4  21115  cnclsi  21124  isreg2  21229  discmp  21249  cmpcld  21253  uncmp  21254  sscmp  21256  hauscmplem  21257  cmpfi  21259  iunconnlem  21278  clsconn  21281  2ndcctbss  21306  restnlly  21333  llyrest  21336  nllyrest  21337  llyidm  21339  nllyidm  21340  cldllycmp  21346  dislly  21348  comppfsc  21383  llycmpkgen2  21401  ptbasfi  21432  txnlly  21488  txcmplem1  21492  tx1stc  21501  xkococnlem  21510  qtopval2  21547  basqtop  21562  tgqtop  21563  qtoprest  21568  kqreglem1  21592  kqreglem2  21593  kqnrmlem1  21594  kqnrmlem2  21595  fsubbas  21718  fgabs  21730  fbasrn  21735  trfil2  21738  trfg  21742  isufil2  21759  trufil  21761  ssufl  21769  ufileu  21770  filufint  21771  fmfnfmlem4  21808  fmfnfm  21809  flimss2  21823  flimss1  21824  fclsfnflim  21878  flimfnfcls  21879  fclscmp  21881  cnpfcfi  21891  alexsubALT  21902  clssubg  21959  clsnsg  21960  tsmsres  21994  ustexsym  22066  ustex2sym  22067  ustex3sym  22068  ustund  22072  ustneism  22074  trust  22080  utoptop  22085  restutopopn  22089  utop2nei  22101  utopreg  22103  cfiluweak  22146  neipcfilu  22147  blssps  22276  blss  22277  blcld  22357  blsscls  22359  met1stc  22373  met2ndci  22374  metust  22410  cfilucfil  22411  restmetu  22422  tgqioo  22650  xrsblre  22661  reconnlem2  22677  xrge0gsumle  22683  xrge0tsms  22684  rescncf  22747  cnmpt2pc  22774  cnheibor  22801  cnllycmp  22802  lebnum  22810  phtpycn  22829  cfilfcls  23118  iscmet3lem2  23136  cmetss  23159  cncmet  23165  bcthlem4  23170  bcth3  23174  rrxcph  23226  rrxmetlem  23236  minveclem4a  23247  minveclem4  23249  ivthicc  23273  ovollb  23293  ovollb2lem  23302  ovollb2  23303  nulmbl2  23350  ioorcl2  23386  uniioombllem3  23399  uniioombllem4  23400  uniioombllem5  23401  opnmbllem  23415  volcn  23420  volivth  23421  mbfeqalem  23454  itg10a  23522  mbfi1fseqlem4  23530  ditgcl  23667  ditgswap  23668  ditgsplitlem  23669  limcflf  23690  limcres  23695  dvbss  23710  dvbsss  23711  perfdvf  23712  dvreslem  23718  dvres2lem  23719  dvres3  23722  dvcnp  23727  dvcnp2  23728  dvcn  23729  dvnff  23731  dvn2bss  23738  dvnres  23739  cpnord  23743  dvaddbr  23746  dvmulbr  23747  dvcobr  23754  dvnfre  23760  dvmptres2  23770  dvmptntr  23779  dvcnvlem  23784  dvcnv  23785  dvferm1lem  23792  dvferm2lem  23794  dvlip  23801  dvlipcn  23802  dvlip2  23803  c1liplem1  23804  dvgt0lem1  23810  lhop1lem  23821  lhop  23824  dvcnvrelem1  23825  dvcnvrelem2  23826  dvcnvre  23827  dvfsumle  23829  dvfsumge  23830  dvfsumabs  23831  ftc1lem1  23843  ftc1lem2  23844  ftc1a  23845  ftc1lem4  23847  ftc2ditglem  23853  itgsubstlem  23856  ig1peu  23976  ig1pdvds  23981  taylfvallem1  24156  tayl0  24161  taylply2  24167  taylply  24168  dvtaylp  24169  dvntaylp  24170  dvntaylp0  24171  taylthlem1  24172  ulmdvlem1  24199  ulmdvlem3  24201  psercn  24225  pserdvlem2  24227  abelth  24240  xrlimcnp  24740  lgamucov  24809  wilthlem2  24840  sqff1o  24953  chtublem  24981  pntlemq  25335  pntlemf  25339  tglineintmo  25582  ttgcontlem1  25810  pthdlem1  26718  shintcli  28316  shub1  28369  mdslmd1lem1  29312  mdexchi  29322  chirredlem1  29377  mdsymlem5  29394  sumdmdii  29402  sumdmdlem2  29406  xrsupssd  29652  xrge0infssd  29654  xrge0tsmsd  29913  smatrcl  29990  locfinreflem  30035  cmpcref  30045  pnfneige0  30125  esum2d  30283  insiga  30328  sssigagen2  30337  dynkin  30358  dya2iocnei  30472  omsmon  30488  carsgclctunlem1  30507  carsggect  30508  omsmeas  30513  ftc2re  30804  fdvneggt  30806  fdvnegge  30808  reprsuc  30821  reprss  30823  reprlt  30825  reprinfz1  30828  logdivsqrle  30856  hgt750lemb  30862  bnj906  31126  bnj1020  31159  bnj1137  31189  bnj1408  31230  bnj1452  31246  erdszelem7  31305  erdszelem8  31306  erdsze2lem1  31311  connpconn  31343  cvmliftmolem1  31389  cvmlift2lem1  31410  cvmlift2lem9  31419  cvmlift2lem10  31420  cvmlift3lem6  31432  cvmlift3lem7  31433  ss2mcls  31591  dftrpred3g  31857  sssslt1  32031  sssslt2  32032  scutbdaybnd  32046  neibastop2lem  32480  fnemeet2  32487  fnejoin1  32488  ontgval  32555  unbdqndv1  32624  opnmbllem0  33575  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  sstotbnd2  33703  heiborlem1  33740  heiborlem8  33747  intidl  33958  lsmsat  34613  lssats  34617  lpssat  34618  lssatle  34620  lssat  34621  lsatcvatlem  34654  paddss12  35423  paddasslem17  35440  pmodlem1  35450  pmod1i  35452  pmodl42N  35455  elpcliN  35497  pclfinN  35504  polcon3N  35521  polcon2N  35523  paddunN  35531  pclfinclN  35554  poml5N  35558  osumcllem1N  35560  osumcllem2N  35561  osumcllem3N  35562  pl42lem2N  35584  pl42lem4N  35586  cdlemn5pre  36806  dihord1  36824  dihord2a  36825  dihord2b  36826  dihord5b  36865  dochss  36971  dochdmj1  36996  djhsumss  37013  djhunssN  37015  dochexmidlem2  37067  lclkrslem1  37143  lclkrslem2  37144  lcfrlem2  37149  elrfi  37574  ismrcd1  37578  istopclsd  37580  mrefg2  37587  aomclem2  37942  aomclem6  37946  hbtlem6  38016  hbt  38017  mptrcllem  38237  dfrcl2  38283  relexp0a  38325  trclimalb2  38335  frege81d  38356  k0004ss2  38767  imo72b2lem0  38782  imo72b2lem2  38784  imo72b2lem1  38788  imo72b2  38792  uzwo4  39535  ssin0  39537  ixpssmapc  39557  ssinc  39578  ssdec  39579  supxrre3  39854  uzfissfz  39855  ssuzfz  39878  ssrexr  39972  supminfxr  40007  inficc  40079  ressiocsup  40099  ressioosup  40100  ressiooinf  40102  limccog  40170  limclner  40201  limsuppnfdlem  40251  limsupres  40255  limsupresuz2  40259  limsupequzlem  40272  limsupvaluz2  40288  supcnvlimsup  40290  limsupgtlem  40327  liminfresuz2  40337  cncfmptssg  40401  cncfuni  40417  icccncfext  40418  dvresntr  40450  dvmptresicc  40452  dvbdfbdioolem1  40461  dvdmsscn  40469  dvnxpaek  40475  dvnprodlem2  40480  stoweidlem59  40594  fourierdlem20  40662  fourierdlem42  40684  fourierdlem48  40689  fourierdlem49  40690  fourierdlem52  40693  fourierdlem58  40699  fourierdlem64  40705  fourierdlem73  40714  fourierdlem76  40717  fourierdlem80  40721  fourierdlem84  40725  fourierdlem93  40734  fourierdlem103  40744  fourierdlem104  40745  fourierdlem113  40754  etransclem18  40787  ioorrnopnlem  40842  salincl  40861  intsal  40866  fsumlesge0  40912  sge0cl  40916  sge0supre  40924  sge0less  40927  sge0split  40944  sge0seq  40981  caragensspw  41044  omessre  41045  caragendifcl  41049  caratheodorylem1  41061  0ome  41064  omess0  41069  caragencmpl  41070  hoicvr  41083  hoissrrn  41084  hoicvrrex  41091  ovnlecvr  41093  ovnsslelem  41095  ovnssle  41096  ovnsubaddlem1  41105  hoissrrn2  41113  hoidmv1lelem1  41126  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem4  41133  ovnlecvr2  41145  voncmpl  41156  hspmbl  41164  opnvonmbllem1  41167  ovolval5lem2  41188  ovolval5lem3  41189  vonioolem1  41215  pimdecfgtioc  41246  pimincfltioc  41247  pimdecfgtioo  41248  pimincfltioo  41249  issmflem  41257  cnfsmf  41270  incsmflem  41271  smfsssmf  41273  smfadd  41294  decsmflem  41295  smflim  41306  smfres  41318  smfmul  41323  smfpimbor1lem1  41326  smfco  41330  smfsuplem1  41338  smfsuplem3  41340  smflimsuplem1  41347  smflimsuplem4  41350  smflimsuplem7  41353  subsubmgm  42122  setrecsss  42772  elpglem1  42782
  Copyright terms: Public domain W3C validator