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

Theorem sstri 3463
Description: Subclass transitivity inference. (Contributed by NM, 5-May-2000.)
Hypotheses
Ref Expression
sstri.1  |-  A  C_  B
sstri.2  |-  B  C_  C
Assertion
Ref Expression
sstri  |-  A  C_  C

Proof of Theorem sstri
StepHypRef Expression
1 sstri.1 . 2  |-  A  C_  B
2 sstri.2 . 2  |-  B  C_  C
3 sstr2 3461 . 2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
41, 2, 3mp2 9 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3433  df-ss 3440
This theorem is referenced by:  snsstp1  4122  snsstp2  4123  uniintsn  4263  ssrnres  5374  cossxp  5458  foimacnv  5756  ssimaex  5855  riotassuniOLD  6188  oprabss  6276  dmexg  6609  rnexg  6610  fabexg  6633  fparlem3  6774  fparlem4  6775  snopsuppss  6805  tposssxp  6849  mapsspw  7348  sbthlem5  7525  sbthlem7  7527  cnvimamptfin  7713  marypha1lem  7784  ordtypelem4  7836  hartogslem1  7857  tc2  8063  tz9.12lem1  8095  rankval4  8175  rankxpl  8183  rankmapu  8186  rankxplim  8187  infxpenlem  8281  ackbij1lem18  8507  cflm  8520  fin23lem29  8611  hsmexlem4  8699  hsmexlem5  8700  brdom3  8796  brdom5  8797  brdom4  8798  smobeth  8851  pwfseqlem3  8928  wundm  8996  wunrn  8997  wunex2  9006  ltsopi  9158  dmaddpi  9160  dmmulpi  9161  nqerf  9200  ltrelxr  9539  nnsscn  10428  nn0sscn  10685  uzwo2  11020  uzinfmi  11035  infmssuzle  11038  infmssuzcl  11039  uzwo3  11049  nn0ssq  11062  nnssq  11063  qsscn  11065  rpnnen1lem3  11082  rpnnen1lem5  11084  dflt2  11226  fzval2  11541  fzof  11651  fzossnn  11695  fzo0ssnn0  11712  injresinj  11740  flval3  11764  uzsup  11803  uzrdgfni  11882  expcl2lem  11978  rpexpcl  11985  expge0  12001  expge1  12002  hashxrcl  12228  seqcoll  12318  wrdexg  12346  seqshft  12676  sqrlem3  12836  limsupval2  13060  limsupgre  13061  rlimpm  13080  rlimclim  13126  isercolllem1  13244  isercolllem2  13245  isercoll  13247  caurcvg  13256  caucvg  13258  summolem2a  13294  summolem2  13295  zsum  13297  fsumcvg3  13308  fsumrpcl  13316  fsumge0  13360  climfsum  13385  ackbijnn  13393  divalglem8  13706  sadaddlem  13764  isprm3  13874  maxprmfct  13901  pclem  14007  prmreclem1  14079  prmreclem2  14080  prmreclem3  14081  1arith  14090  4sqlem11  14118  ramtlecl  14163  ramcl2lem  14172  ramxrcl  14180  cshwshashlem1  14224  structfn  14289  strlemor1  14367  strleun  14370  srngbase  14396  srngplusg  14397  srngmulr  14398  lmodbase  14405  lmodplusg  14406  lmodsca  14407  ipsbase  14412  ipsaddg  14413  ipsmulr  14414  ipssca  14415  ipsvsca  14416  ipsip  14417  phlbase  14422  phlplusg  14423  phlsca  14424  phlvsca  14425  phlip  14426  odrngbas  14448  odrngplusg  14449  odrngmulr  14450  odrngtset  14451  odrngle  14452  odrngds  14453  prdsval  14495  prdssca  14496  prdsbas  14497  prdsplusg  14498  prdsmulr  14499  prdsvsca  14500  prdsip  14501  prdsle  14502  prdsds  14504  prdstset  14506  prdshom  14507  prdsco  14508  imasbas  14552  imasds  14553  imasplusg  14557  imasmulr  14558  imassca  14559  imasvsca  14560  imasip  14561  imastset  14562  imasle  14563  wunfunc  14911  fullfunc  14918  fthfunc  14919  isfull  14922  isfth  14926  wunnat  14968  dmcoass  15036  catcisolem  15076  catciso  15077  catcoppccl  15078  catcfuccl  15079  catcxpccl  15119  ipobas  15427  ipolerval  15428  ipotset  15429  psdmrn  15479  psss  15486  ledm  15496  lern  15497  dirdm  15506  dirge  15509  mvdco  16053  f1omvdconj  16054  gexex  16439  gsumval3OLD  16486  gsumval3  16489  gsumzaddlemOLD  16514  lssacs  17154  asplss  17506  aspsubrg  17508  psrass1lem  17553  psrbas  17554  psrbasOLD  17555  psrplusg  17558  psrmulr  17561  psrsca  17566  psrvscafval  17567  psrass1  17584  psrdi  17585  psrdir  17586  psrass23l  17587  psrcom  17588  psrass23  17589  psropprmul  17800  coe1mul2  17830  cnfldbas  17931  cnfldadd  17932  cnfldmul  17933  cnfldcj  17934  cnfldtset  17935  cnfldle  17936  cnfldds  17937  cnfldunif  17938  rge0srg  17991  zntoslem  18098  ofco2  18443  leordtval2  18932  lmbrf  18980  lmres  19020  fiuncmp  19123  1stckgenlem  19242  kgencn3  19247  ptbasfi  19270  xkoopn  19278  txcnmpt  19313  txkgen  19341  opnfbas  19531  fmfnfmlem4  19646  tsmsxplem1  19843  trust  19920  restutop  19928  nmoffn  20406  nmofval  20409  nmogelb  20411  nmolb  20412  nmof  20414  qtopbas  20454  tgqioo  20493  re2ndc  20494  iitopon  20571  dfii3  20575  iimulcn  20626  cnheiborlem  20642  bndth  20646  lebnumii  20654  reparphti  20685  pcoass  20712  cphsqrcl  20819  lmmbrf  20889  iscauf  20907  caucfil  20910  lmclimf  20930  rrxmval  21020  rrxmet  21023  ovolfioo  21067  ovolficc  21068  ovolficcss  21069  ovolfsf  21071  ovollb  21078  ovolicc2lem3  21118  ovolicc2lem4  21119  ovolicc2  21121  volf  21128  volsup  21153  ovolfs2  21167  uniiccdif  21174  uniioovol  21175  uniiccvol  21176  uniioombllem2  21179  uniioombllem3a  21180  uniioombllem3  21181  uniioombllem4  21182  uniioombllem5  21183  uniioombl  21185  dyadmbllem  21195  dyadmbl  21196  opnmbllem  21197  opnmblALT  21199  volsup2  21201  vitalilem4  21207  vitalilem5  21208  vitali  21209  mbfimaopnlem  21249  mbflimsup  21260  i1f0  21281  i1f1  21284  itg11  21285  itg2mulc  21341  itg2gt0  21354  ellimc2  21468  limcresi  21476  dvreslem  21500  dvres2lem  21501  dvaddbr  21528  dvmulbr  21529  dvlipcn  21582  c1liplem1  21584  lhop1lem  21601  lhop1  21602  lhop2  21603  lhop  21604  dvfsumrlim  21619  ftc1cn  21631  itgsubstlem  21636  itgsubst  21637  mdegleb  21651  mdeglt  21652  mdegldg  21653  mdegxrcl  21654  mdegcl  21656  mdegaddle  21661  mdegmullem  21665  deg1mul3le  21704  ig1peu  21759  ig1pdvds  21764  aacjcl  21909  aannenlem2  21911  aannenlem3  21912  aalioulem2  21915  taylfval  21940  radcnvcl  21998  radcnvlt1  21999  radcnvle  22001  abelth  22022  abelth2  22023  pilem2  22033  pilem3  22034  pige3  22095  recosf1o  22107  resinf1o  22108  tanord1  22109  logcn  22208  dvlog  22212  dvlog2lem  22213  efopn  22219  logtayl  22221  cxpcn3  22302  loglesqr  22312  ssscongptld  22336  leibpi  22453  efrlim  22479  jensenlem1  22496  jensenlem2  22497  jensen  22498  amgm  22500  ftalem5  22530  efnnfsumcl  22556  efchtdvds  22613  dvdsmulf1o  22650  fsumdvdsmul  22651  lgsfcl2  22757  2sqlem6  22824  2sqlem8  22827  2sqlem9  22828  rpvmasumlem  22852  rpvmasum2  22877  dchrisum0re  22878  dchrisum0lem3  22884  dchrisum0  22885  rplogsum  22892  dirith2  22893  axtgcgrrflx  23039  axtgcgrid  23040  axtgsegcon  23041  axtg5seg  23042  axtgbtwnid  23043  axtgpasch  23044  axtgcont1  23045  tglng  23099  umgrass  23388  constr3pthlem1  23676  nmlno0lem  24328  hlimcaui  24774  chsspwh  24785  shsss  24851  chintcli  24869  shsleji  24908  shub1i  24912  shsval2i  24925  lejdii  25076  spanuni  25082  sshhococi  25084  spansnpji  25116  osumcori  25181  5oai  25199  3oalem6  25205  3oai  25206  pjssmii  25219  mayete3i  25266  mayete3iOLD  25267  mayetes3i  25268  nmlnop0iALT  25534  imaelshi  25597  pjnmopi  25687  pjclem1  25734  pjci  25739  mdslmd1lem1  25864  shatomistici  25900  hatomistici  25901  chpssati  25902  xppreima  26098  iundisjfi  26214  iundisj2fi  26215  xrsmulgzz  26273  fsumrp0cl  26292  gsumunsnf  26379  gsumle  26380  gsummpt2co  26383  xrge0slmod  26446  unitsscn  26460  ordtconlem1  26488  xrge0iifhom  26501  lmlimxrge0  26512  lmxrge0  26516  esumcst  26648  esumpfinvallem  26657  esumpfinval  26658  esumpfinvalf  26659  esumcvg  26669  measunl  26764  imambfm  26811  elmbfmvol2  26816  sxbrsigalem3  26821  sxbrsigalem2  26835  sxbrsigalem4  26836  sitgclg  26862  eulerpartlem1  26884  eulerpartlemgvv  26893  eulerpartlemgh  26895  eulerpartlemgf  26896  ballotlemfc0  27009  ballotlemfcc  27010  ballotlemiex  27018  ballotlemsup  27021  ballotlemsdom  27028  ballotlemsima  27032  ballotlemrv2  27038  ballotth  27054  signsplypnf  27085  signsply0  27086  lgamgulmlem2  27150  subfacp1lem2a  27202  erdszelem4  27216  erdszelem5  27217  erdszelem7  27219  erdszelem8  27220  kur14lem7  27234  kur14lem9  27236  cvxpcon  27265  cvxscon  27266  rescon  27269  iccllyscon  27273  prodmolem2a  27581  prodmolem2  27582  zprod  27584  fprodrpcl  27603  rprisefaccl  27660  txpss3v  28043  txprel  28044  limitssson  28076  onint1  28429  opnmbllem0  28565  mblfinlem1  28566  mblfinlem2  28567  mblfinlem3  28568  mblfinlem4  28569  ismblfin  28570  mbfposadd  28577  cnambfre  28578  itg2addnc  28584  ftc1cnnclem  28603  ftc1cnnc  28604  ftc1anclem3  28607  ftc1anclem7  28611  ftc1anc  28613  ftc2nc  28614  dvreasin  28620  dvreacos  28621  areacirclem1  28622  areacirclem2  28623  areacirc  28627  finminlem  28651  comppfsc  28717  tailf  28734  filnetlem3  28739  caures  28794  reheibor  28876  diophin  29249  4rexfrabdioph  29274  6rexfrabdioph  29275  irrapxlem1  29301  irrapx1  29307  monotuz  29420  jm2.27dlem5  29500  hbtlem2  29618  algbase  29673  algaddg  29674  algmulr  29675  algsca  29676  algvsca  29677  itgpowd  29728  arearect  29729  areaquad  29730  lhe4.4ex1a  29741  itgsin0pilem1  29928  itgsinexplem1  29932  itgsinexp  29933  wallispilem2  29999  disjxwwlkn  30702  relopabVD  31937  bnj1145  32284  bnj1286  32310  bj-unrab  32729  bj-2upln1upl  32817  bj-rrvecsscmn  32894  atlatmstc  33270  atlatle  33271  pmaple  33711  sspadd1  33765  sspadd2  33766  taupilem2  35922  taupi  35923
  Copyright terms: Public domain W3C validator