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

Theorem sstrd 3499
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 3497 . 2  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475
This theorem is referenced by:  syl5ss  3500  syl6ss  3501  ssdif2d  3628  uniintsn  4309  funss  5596  fssxp  5733  knatar  6238  suppssfvOLD  6516  suppssov1OLD  6517  tfisi  6678  suppfnss  6927  suppssov1  6934  suppssfv  6938  tposss  6958  tfrlem1  7047  omwordri  7223  oewordri  7243  oeeui  7253  oaabs2  7296  omopthlem1  7306  ecinxp  7388  sbthlem1  7629  dffi2  7885  hartogslem1  7970  cantnfcl  8089  cantnflt  8094  cantnfp1lem3  8102  cantnflem3  8113  cantnfclOLD  8119  cantnfltOLD  8124  cantnfp1lem3OLD  8128  cantnflem3OLD  8135  cnfcom  8147  cnfcom3lem  8150  cnfcomOLD  8155  cnfcom3lemOLD  8158  rankssb  8269  tskwe  8334  dfac12lem2  8527  dfac12lem3  8528  cfflb  8642  cfcof  8657  ssfin2  8703  hsmexlem4  8812  ttukeylem6  8897  ttukeylem7  8898  fpwwe2lem1  9012  fpwwe2lem8  9018  fpwwe2lem11  9021  fpwwe2lem12  9022  canthnumlem  9029  canthwelem  9031  canthwe  9032  canthp1lem2  9034  pwfseqlem5  9044  wunex2  9119  tsktrss  9142  inttsk  9155  uzwo3  11188  supicc  11679  supiccub  11680  supicclub  11681  seqsplit  12122  seqf1olem2a  12127  seqz  12137  swrdval2  12629  sumss  13528  qshash  13621  incexc  13631  incexc2  13632  prodss  13736  rpnnen2lem11  13940  vdwlem1  14481  ramub1lem1  14526  imasaddvallem  14908  imasvscaf  14918  mrerintcl  14976  ismred2  14982  mremre  14983  mrcuni  15000  mressmrcd  15006  submrc  15007  mrissmrid  15020  mreexexlem2d  15024  isacs2  15032  isacs1i  15036  invss  15137  ssctr  15176  funcres2b  15245  isacs3lem  15775  acsfiindd  15786  acsmapd  15787  acsmap2d  15788  tsrdir  15847  subsubm  15967  gsumwspan  15993  subsubg  16203  subgint  16204  cntzidss  16354  symggen  16474  pmtrdifellem1  16480  pmtrdifellem2  16481  pgpssslw  16613  lsmless1x  16643  lsmless2x  16644  lsmless12  16660  subglsm  16670  gsumval3OLD  16887  gsumval3lem2  16889  gsumzaddlem  16913  gsumzadd  16914  gsumzaddOLD  16916  gsum2d  16978  gsum2dOLD  16979  dmdprdd  17009  dprdfeq0  17041  dprdfeq0OLD  17048  dprdspan  17053  dprdres  17054  dprdss  17055  dprdz  17056  subgdmdprd  17060  subgdprd  17061  dprdsn  17062  dprd2dlem1  17069  dprd2da  17070  dmdprdsplit2lem  17073  dprdsplit  17076  pgpfac1lem2  17105  pgpfac1lem3  17107  pgpfac1lem5  17109  subsubrg  17434  lspss  17609  lspun  17612  lsslsp  17640  lmhmlsp  17674  lsmelval2  17710  lsmssspx  17713  lsppratlem2  17773  lsppratlem3  17774  lsppratlem4  17775  lbsextlem2  17784  lbsextlem3  17785  aspss  17960  ocvlsp  18685  cssmre  18702  obselocv  18737  obslbs  18739  toponmre  19572  neiint  19583  neiss  19588  lpss  19621  lpss3  19623  restopnb  19654  restfpw  19658  neitr  19659  restcls  19660  restntr  19661  restlp  19662  ordtbas  19671  pnfnei  19699  mnfnei  19700  iscnp4  19742  cnclsi  19751  isreg2  19856  discmp  19876  cmpcld  19880  uncmp  19881  sscmp  19883  hauscmplem  19884  cmpfi  19886  iunconlem  19906  clscon  19909  2ndcctbss  19934  restnlly  19961  llyrest  19964  nllyrest  19965  llyidm  19967  nllyidm  19968  cldllycmp  19974  dislly  19976  comppfsc  20011  llycmpkgen2  20029  ptbasfi  20060  txnlly  20116  txcmplem1  20120  tx1stc  20129  xkococnlem  20138  qtopval2  20175  basqtop  20190  tgqtop  20191  qtoprest  20196  kqreglem1  20220  kqreglem2  20221  kqnrmlem1  20222  kqnrmlem2  20223  fsubbas  20346  fgabs  20358  fbasrn  20363  trfil2  20366  trfg  20370  isufil2  20387  trufil  20389  ssufl  20397  ufileu  20398  filufint  20399  fmfnfmlem4  20436  fmfnfm  20437  flimss2  20451  flimss1  20452  fclsfnflim  20506  flimfnfcls  20507  fclscmp  20509  cnpfcfi  20519  alexsubALT  20529  clssubg  20585  clsnsg  20586  tsmsres  20624  ustexsym  20696  ustex2sym  20697  ustex3sym  20698  ustund  20702  ustneism  20704  trust  20710  utoptop  20715  restutopopn  20719  utop2nei  20731  utopreg  20733  cfiluweak  20776  neipcfilu  20777  blssps  20905  blss  20906  blcld  20986  blsscls  20988  met1stc  21002  met2ndci  21003  metustOLD  21048  metust  21049  cfilucfilOLD  21050  cfilucfil  21051  restmetu  21068  tgqioo  21283  xrsblre  21294  reconnlem2  21310  xrge0gsumle  21316  xrge0tsms  21317  rescncf  21379  cnmpt2pc  21406  cnheibor  21433  cnllycmp  21434  lebnum  21442  phtpycn  21461  cfilfcls  21691  iscmet3lem2  21709  cmetss  21731  cncmet  21739  bcthlem4  21744  bcth3  21748  rrxcph  21802  rrxmetlem  21812  minveclem4a  21823  minveclem4  21825  ivthicc  21848  ovollb  21868  ovollb2lem  21877  ovollb2  21878  nulmbl2  21925  ioorcl2  21959  uniioombllem3  21972  uniioombllem4  21973  uniioombllem5  21974  opnmbllem  21988  volcn  21993  volivth  21994  mbfeqalem  22027  itg10a  22095  mbfi1fseqlem4  22103  ditgcl  22240  ditgswap  22241  ditgsplitlem  22242  limcflf  22263  limcres  22268  dvbss  22283  dvbsss  22284  perfdvf  22285  dvreslem  22291  dvres2lem  22292  dvres3  22295  dvcnp  22300  dvcnp2  22301  dvcn  22302  dvnff  22304  dvn2bss  22311  dvnres  22312  cpnord  22316  dvaddbr  22319  dvmulbr  22320  dvcobr  22327  dvnfre  22333  dvmptres2  22343  dvmptntr  22352  dvcnvlem  22355  dvcnv  22356  dvferm1lem  22363  dvferm2lem  22365  dvlip  22372  dvlipcn  22373  dvlip2  22374  c1liplem1  22375  dvgt0lem1  22381  lhop1lem  22392  lhop  22395  dvcnvrelem1  22396  dvcnvrelem2  22397  dvcnvre  22398  dvfsumle  22400  dvfsumge  22401  dvfsumabs  22402  ftc1lem1  22414  ftc1lem2  22415  ftc1a  22416  ftc1lem4  22418  ftc2ditglem  22424  itgsubstlem  22427  ig1peu  22550  ig1pdvds  22555  taylfvallem1  22730  tayl0  22735  taylply2  22741  taylply  22742  dvtaylp  22743  dvntaylp  22744  dvntaylp0  22745  taylthlem1  22746  ulmdvlem1  22773  ulmdvlem3  22775  psercn  22799  pserdvlem2  22801  abelth  22814  xrlimcnp  23276  wilthlem2  23321  sqff1o  23434  chtublem  23464  pntlemq  23764  pntlemf  23768  tglineintmo  24000  ttgcontlem1  24166  ghsubgolemOLD  25350  shintcli  26225  shub1  26278  mdslmd1lem1  27222  mdexchi  27232  chirredlem1  27287  mdsymlem5  27304  sumdmdii  27312  sumdmdlem2  27316  xrsupssd  27557  xrge0infssd  27559  xrge0tsmsd  27753  locfinreflem  27821  cmpcref  27831  pnfneige0  27911  insiga  28115  sssigagen2  28124  dya2iocnei  28231  omsmon  28245  lgamucov  28558  erdszelem7  28619  erdszelem8  28620  erdsze2lem1  28625  conpcon  28658  cvmliftmolem1  28704  cvmlift2lem1  28725  cvmlift2lem9  28734  cvmlift2lem10  28735  cvmlift3lem6  28747  cvmlift3lem7  28748  ss2mcls  28906  rtrclreclem.min  29048  dftrpred3g  29292  nofulllem3  29440  ontgval  29872  opnmbllem0  30026  ftc1anclem7  30072  ftc1anclem8  30073  ftc1anc  30074  neibastop2lem  30154  fnemeet2  30161  fnejoin1  30162  sstotbnd2  30246  heiborlem1  30283  heiborlem8  30290  intidl  30402  elrfi  30602  ismrcd1  30606  istopclsd  30608  mrefg2  30615  aomclem2  30977  aomclem6  30981  hbtlem6  31054  hbt  31055  limccog  31580  limclner  31611  cncfmptssg  31626  cncfuni  31643  icccncfext  31644  dvresntr  31667  dvmptresicc  31670  dvbdfbdioolem1  31679  dvdmsscn  31687  dvnxpaek  31693  dvnprodlem2  31698  stoweidlem59  31795  fourierdlem20  31863  fourierdlem42  31885  fourierdlem48  31891  fourierdlem49  31892  fourierdlem52  31895  fourierdlem58  31901  fourierdlem64  31907  fourierdlem73  31916  fourierdlem76  31919  fourierdlem80  31923  fourierdlem84  31927  fourierdlem93  31936  fourierdlem103  31946  fourierdlem104  31947  fourierdlem113  31956  etransclem18  31989  etransclem46  32017  etransclem48  32019  subsubmgm  32439  bnj906  33856  bnj1020  33889  bnj1137  33919  bnj1408  33960  bnj1452  33976  lsmsat  34608  lssats  34612  lpssat  34613  lssatle  34615  lssat  34616  lsatcvatlem  34649  paddss12  35418  paddasslem17  35435  pmodlem1  35445  pmod1i  35447  pmodl42N  35450  elpcliN  35492  pclfinN  35499  polcon3N  35516  polcon2N  35518  paddunN  35526  pclfinclN  35549  poml5N  35553  osumcllem1N  35555  osumcllem2N  35556  osumcllem3N  35557  pl42lem2N  35579  pl42lem4N  35581  cdlemn5pre  36802  dihord1  36820  dihord2a  36821  dihord2b  36822  dihord5b  36861  dochss  36967  dochdmj1  36992  djhsumss  37009  djhunssN  37011  dochexmidlem2  37063  lclkrslem1  37139  lclkrslem2  37140  lcfrlem2  37145  trrelssd  37605  imo72b2lem0  37786  imo72b2lem2  37788  imo72b2lem1  37792  imo72b2  37797
  Copyright terms: Public domain W3C validator