Theorem sstri 3944

Description: Subclass transitivity inference. (Contributed by NM, 5-May-2000.)

Hypotheses

Ref	Expression
sstri.1	⊢ 𝐴 ⊆ 𝐵
sstri.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
sstri	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem sstri

Step	Hyp	Ref	Expression
1		sstri.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		sstri.2	. 2 ⊢ 𝐵 ⊆ 𝐶
3		sstr2 3941	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
4	1, 2, 3	mp2 9	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 207  df-ss 3919

This theorem is referenced by:  snsstp1  4768  snsstp2  4769  uniintsn  4935  elopabran  5501  ssrnres  6125  cossxp  6219  foimacnv  6780  ssimaex  6907  riotassuni  7343  oprabss  7454  dmexg  7831  rnexg  7832  fabexgOLD  7869  mptmpoopabbrd  8012  fparlem3  8044  fparlem4  8045  snopsuppss  8109  tposssxp  8160  naddunif  8608  naddasslem1  8609  naddasslem2  8610  mapsspw  8802  sbthlem5  9004  sbthlem7  9006  cnvimamptfin  9237  marypha1lem  9317  ordtypelem4  9407  hartogslem1  9428  ttrclco  9608  cottrcl  9609  tc2  9630  frmin  9642  frrlem16  9651  tz9.12lem1  9680  rankval4  9760  rankxpl  9768  rankmapu  9771  rankxplim  9772  djuin  9811  infxpenlem  9904  ackbij1lem18  10127  cflm  10141  fin23lem29  10232  hsmexlem4  10320  hsmexlem5  10321  brdom3  10419  brdom5  10420  brdom4  10421  smobeth  10477  pwfseqlem3  10551  wundm  10619  wunrn  10620  wunex2  10629  ltsopi  10779  dmaddpi  10781  dmmulpi  10782  nqerf  10821  ltrelxr  11173  uzssre  12754  uzwo2  12810  infssuzle  12829  infssuzcl  12830  uzwo3  12841  nn0ssq  12855  nnssq  12856  qsscn  12858  rpnnen1lem3  12877  rpnnen1lem5  12879  dflt2  13047  ioosscn  13308  unitsscn  13400  fzval2  13410  fzossz  13579  fzossnn  13611  injresinj  13691  flval3  13719  uzsup  13767  uzrdgfni  13865  expcl2lem  13980  rpexpcl  13987  expge0  14005  expge1  14006  hashxrcl  14264  seqcoll  14371  xptrrel  14887  trclublem  14902  01sqrexlem3  15151  limsupval2  15387  limsupgre  15388  rlimpm  15407  rlimclim  15453  isercolllem1  15572  isercolllem2  15573  isercoll  15575  caurcvg  15584  caucvg  15586  summolem2a  15622  summolem2  15623  zsum  15625  fsumcvg3  15636  fsumrpcl  15644  fsumge0  15702  climfsum  15727  ackbijnn  15735  prodmolem2a  15841  prodmolem2  15842  zprod  15844  fprodrpcl  15863  fprodge0  15900  fprodge1  15902  rprisefaccl  15930  divalglem8  16311  sadaddlem  16377  lcmfval  16532  isprm3  16594  maxprmfct  16620  pclem  16750  prmreclem1  16828  prmreclem2  16829  prmreclem3  16830  1arith  16839  4sqlem11  16867  ramtlecl  16912  ramcl2lem  16921  ramxrcl  16929  prmgaplem3  16965  prmgaplem4  16966  cshwshashlem1  17007  structfn  17067  strleun  17068  ressbasss  17150  ressbasss2  17152  srngbase  17214  srngplusg  17215  srngmulr  17216  lmodbase  17230  lmodplusg  17231  lmodsca  17232  ipsbase  17241  ipsaddg  17242  ipsmulr  17243  ipssca  17244  ipsvsca  17245  ipsip  17246  phlbase  17251  phlplusg  17252  phlsca  17253  phlvsca  17254  phlip  17255  odrngbas  17308  odrngplusg  17309  odrngmulr  17310  odrngtset  17311  odrngle  17312  odrngds  17313  prdsvallem  17358  prdsval  17359  prdssca  17360  prdsbas  17361  prdsplusg  17362  prdsmulr  17363  prdsvsca  17364  prdsip  17365  prdsle  17366  prdsds  17368  prdstset  17370  prdshom  17371  prdsco  17372  imasbas  17416  imasds  17417  imasplusg  17421  imasmulr  17422  imassca  17423  imasvsca  17424  imasip  17425  imastset  17426  imasle  17427  wunfunc  17808  fullfunc  17815  fthfunc  17816  isfull  17819  isfth  17823  wunnat  17866  dmcoass  17973  catcisolem  18017  catciso  18018  catcoppccl  18024  catcfuccl  18025  catcxpccl  18113  ipobas  18437  ipolerval  18438  ipotset  18439  psdmrn  18479  psss  18486  ledm  18496  lern  18497  dirdm  18506  dirge  18509  mulgfval  18982  mvdco  19358  f1omvdconj  19359  gexex  19766  gsumval3  19820  lssacs  20901  cnfldbas  21296  mpocnfldadd  21297  mpocnfldmul  21299  cnfldcj  21301  cnfldtset  21302  cnfldle  21303  cnfldds  21304  cnfldunif  21305  cnfldbasOLD  21311  cnfldaddOLD  21312  cnfldmulOLD  21313  cnfldcjOLD  21314  cnfldtsetOLD  21315  cnfldleOLD  21316  cnflddsOLD  21317  cnfldunifOLD  21318  rge0srg  21376  zntoslem  21494  asplss  21812  aspsubrg  21814  psrass1lem  21870  psrbas  21871  psrplusg  21874  psrmulr  21880  psrsca  21885  psrvscafval  21886  psrass1  21902  psrass23l  21905  psrcom  21906  psrass23  21907  psropprmul  22151  coe1mul2  22184  ofco2  22367  toponsspwpw  22838  dmtopon  22839  leordtval2  23128  lmbrf  23176  lmres  23216  fiuncmp  23320  comppfsc  23448  1stckgenlem  23469  kgencn3  23474  ptbasfi  23497  xkoopn  23505  txcnmpt  23540  txkgen  23568  opnfbas  23758  fmfnfmlem4  23873  tsmsxplem1  24069  trust  24145  restutop  24153  nmoffn  24627  nmofval  24630  nmogelb  24632  nmolb  24633  nmof  24635  qtopbas  24675  tgqioo  24716  re2ndc  24717  iitopon  24800  dfii3  24804  iimulcnOLD  24863  cnheiborlem  24881  bndth  24885  lebnumii  24893  reparphtiOLD  24925  pcoass  24952  cphsqrtcl  25112  lmmbrf  25190  iscauf  25208  caucfil  25211  lmclimf  25232  rrxmval  25333  rrxmet  25336  ovolfioo  25396  ovolficc  25397  ovolficcss  25398  ovolfsf  25400  ovollb  25408  ovolicc2lem3  25448  ovolicc2lem4  25449  ovolicc2  25451  volf  25458  volsup  25485  ovolfs2  25500  uniiccdif  25507  uniioovol  25508  uniiccvol  25509  uniioombllem2  25512  uniioombllem3a  25513  uniioombllem3  25514  uniioombllem4  25515  uniioombllem5  25516  uniioombl  25518  dyadmbllem  25528  dyadmbl  25529  opnmbllem  25530  opnmblALT  25532  volsup2  25534  vitalilem4  25540  vitalilem5  25541  vitali  25542  mbfimaopnlem  25584  mbflimsup  25595  i1f0  25616  i1f1  25619  itg11  25620  itg2mulc  25676  itg2gt0  25689  ellimc2  25806  limcresi  25814  dvreslem  25838  dvres2lem  25839  dvaddbr  25868  dvmulbr  25869  dvmulbrOLD  25870  dvlipcn  25927  c1liplem1  25929  lhop1lem  25946  lhop1  25947  lhop2  25948  lhop  25949  dvfsumrlim  25966  ftc1cn  25978  itgsubstlem  25983  itgsubst  25984  itgpowd  25985  mdegleb  25997  mdeglt  25998  mdegldg  25999  mdegxrcl  26000  mdegcl  26002  mdegaddle  26007  mdegmullem  26011  deg1mul3le  26050  ig1peu  26108  ig1pdvds  26113  aacjcl  26263  aannenlem2  26265  aannenlem3  26266  aalioulem2  26269  taylfval  26294  radcnvcl  26354  radcnvlt1  26355  radcnvle  26357  abelth  26379  abelth2  26380  pilem2  26390  pilem3  26391  pige3ALT  26457  recosf1o  26472  resinf1o  26473  tanord1  26474  logcn  26584  dvlog  26588  dvlog2lem  26589  efopn  26595  logtayl  26597  cxpcn3  26686  loglesqrt  26699  ssscongptld  26760  leibpi  26880  efrlim  26907  efrlimOLD  26908  jensenlem1  26925  jensenlem2  26926  jensen  26927  amgm  26929  lgamgulmlem2  26968  ftalem5  27015  efnnfsumcl  27041  efchtdvds  27097  mpodvdsmulf1o  27132  fsumdvdsmul  27133  dvdsmulf1o  27134  fsumdvdsmulOLD  27135  lgsfcl2  27242  2sqlem6  27362  2sqlem8  27365  2sqlem9  27366  rpvmasumlem  27426  rpvmasum2  27451  dchrisum0re  27452  dchrisum0lem3  27458  dchrisum0  27459  rplogsum  27466  dirith2  27467  noextendseq  27607  oldf  27799  leftssno  27827  rightssno  27828  addsbdaylem  27960  mulsproplem12  28067  mulsproplem13  28068  mulsproplem14  28069  mulsasslem3  28105  precsexlem11  28156  onscutlt  28202  bdayon  28210  nnssno  28252  axtgcgrrflx  28441  axtgcgrid  28442  axtgsegcon  28443  axtg5seg  28444  axtgbtwnid  28445  axtgpasch  28446  axtgcont1  28447  tgcgr4  28510  motcgrg  28523  tglng  28525  upgrss  29067  pthdivtx  29706  disjxwwlkn  29892  ex-fpar  30440  nmlno0lem  30771  hlimcaui  31214  chsspwh  31225  shsss  31291  chintcli  31309  shsleji  31348  shub1i  31352  shsval2i  31365  lejdii  31516  spanuni  31522  sshhococi  31524  spansnpji  31556  osumcori  31621  5oai  31639  3oalem6  31645  3oai  31646  pjssmii  31659  mayete3i  31706  mayetes3i  31707  nmlnop0iALT  31973  imaelshi  32036  pjnmopi  32126  pjclem1  32173  pjci  32178  mdslmd1lem1  32303  shatomistici  32339  hatomistici  32340  chpssati  32341  xppreima  32625  iundisjfi  32776  iundisj2fi  32777  fprodex01  32806  indsumin  32841  xrsmulgzz  32988  fsumrp0cl  33000  gsummpt2co  33026  cycpmfv2  33081  cycpmrn  33110  rlocbas  33232  rlocaddval  33233  rlocmulval  33234  1fldgenq  33286  xrge0slmod  33311  lsmsnorb  33354  idlsrgbas  33467  idlsrgplusg  33468  idlsrgmulr  33470  idlsrgtset  33471  constrextdg2  33760  ordtconnlem1  33935  xrge0iifhom  33948  lmlimxrge0  33959  lmxrge0  33963  esumcst  34074  esumpfinvallem  34085  esumpfinval  34086  esumpfinvalf  34087  esumcvg  34097  imambfm  34273  elmbfmvol2  34278  sxbrsigalem3  34283  sxbrsigalem2  34297  sxbrsigalem4  34298  sitgclg  34353  eulerpartlem1  34378  eulerpartlemgvv  34387  eulerpartlemgh  34389  eulerpartlemgf  34390  ballotlemfc0  34504  ballotlemfcc  34505  ballotlemiex  34513  ballotlemsup  34516  ballotlemsima  34527  ballotlemrv2  34533  ballotth  34549  signsplypnf  34561  signsply0  34562  rpsqrtcn  34604  itgexpif  34617  fsum2dsub  34618  reprfi2  34634  chtvalz  34640  breprexplemc  34643  breprexpnat  34645  circlemeth  34651  circlemethnat  34652  circlevma  34653  circlemethhgt  34654  hgt750lemd  34659  hgt750lema  34668  tgoldbachgtde  34671  tgoldbachgtda  34672  tgoldbachgt  34674  bnj1145  35003  bnj1286  35029  subfacp1lem2a  35222  erdszelem4  35236  erdszelem5  35237  erdszelem7  35239  erdszelem8  35240  kur14lem7  35254  kur14lem9  35256  resconn  35288  iccllysconn  35292  txpss3v  35918  txprel  35919  limitssson  35951  finminlem  36358  tailf  36415  filnetlem3  36420  onint1  36489  bj-unrab  36966  bj-2upln1upl  37064  bj-imdirco  37230  bj-rvecssabl  37346  taupilem2  37362  taupi  37363  poimirlem3  37669  poimirlem30  37696  poimirlem31  37697  poimirlem32  37698  broucube  37700  opnmbllem0  37702  mblfinlem1  37703  mblfinlem2  37704  mblfinlem3  37705  mblfinlem4  37706  ismblfin  37707  mbfposadd  37713  cnambfre  37714  itg2addnc  37720  ftc1cnnclem  37737  ftc1cnnc  37738  ftc1anclem3  37741  ftc1anclem7  37745  ftc1anc  37747  ftc2nc  37748  dvreasin  37752  dvreacos  37753  areacirclem1  37754  areacirclem2  37755  areacirc  37759  caures  37806  reheibor  37885  xrnss3v  38406  xrnrel  38407  atlatmstc  39364  atlatle  39365  pmaple  39806  sspadd1  39860  sspadd2  39861  dvrelog2  42103  dvrelog3  42104  rpsscn  42338  sumcubes  42352  redvmptabs  42399  diophin  42811  4rexfrabdioph  42837  6rexfrabdioph  42838  irrapxlem1  42861  irrapx1  42867  rmxyelqirr  42949  monotuz  42980  jm2.27dlem5  43052  hbtlem2  43163  algbase  43213  algaddg  43214  algmulr  43215  algsca  43216  algvsca  43217  arearect  43254  areaquad  43255  rtrclex  43656  trclubgNEW  43657  trclexi  43659  rtrclexi  43660  cnvtrcl0  43665  dfrtrcl5  43668  trrelsuperrel2dg  43710  relexpaddss  43757  brtrclfv2  43766  frege131d  43803  xphe  43820  clsk3nimkb  44079  gneispace  44173  k0004val0  44193  inaex  44336  lhe4.4ex1a  44368  uzmptshftfval  44385  binomcxplemdvbinom  44392  binomcxplemcvg  44393  binomcxplemnotnn0  44395  relopabVD  44939  dmwf  45004  rnwf  45005  fzisoeu  45347  fzsscn  45358  fzssre  45361  fzossuz  45425  zssxr  45441  uzssre2  45451  supminfxr  45508  uzsscn  45519  rpssxr  45524  uzinico  45605  limcresiooub  45686  limcresioolb  45687  limcleqr  45688  limclner  45695  limclr  45699  limsupequzmpt2  45762  liminfval2  45812  liminfequzmpt2  45835  icccncfext  45931  cncficcgt0  45932  ioodvbdlimc1lem2  45976  ioodvbdlimc2lem  45978  dvnprodlem2  45991  itgsin0pilem1  45994  itgsinexplem1  45998  itgsinexp  45999  dirkercncflem2  46148  fourierdlem16  46167  fourierdlem18  46169  fourierdlem20  46171  fourierdlem21  46172  fourierdlem22  46173  fourierdlem25  46176  fourierdlem37  46188  fourierdlem42  46193  fourierdlem50  46200  fourierdlem52  46202  fourierdlem62  46212  fourierdlem64  46214  fourierdlem66  46216  fourierdlem68  46218  fourierdlem74  46224  fourierdlem75  46225  fourierdlem76  46226  fourierdlem79  46229  fourierdlem83  46233  fourierdlem95  46245  fourierdlem101  46251  fourierdlem102  46252  fourierdlem103  46253  fourierdlem104  46254  fourierdlem112  46262  fourierdlem114  46264  sqwvfoura  46272  sqwvfourb  46273  fouriersw  46275  etransclem24  46302  etransclem48  46326  sge0sn  46423  sge0tsms  46424  sge0f1o  46426  sge0pr  46438  sge0resplit  46450  sge0split  46453  sge0iunmptlemre  46459  sge0isummpt2  46476  carageniuncllem1  46565  hoicvr  46592  hoicvrrex  46600  hoidmvlelem2  46640  hspmbl  46673  smfmullem4  46838  lamberte  46925  rehalfge1  47372  prmdvdsfmtnof1lem1  47621  prmdvdsfmtnof  47623  upgrimpthslem2  47945  upgrimpths  47946  oddibas  48210  2zrngbas  48279  2zrng0  48281  dmtposss  48913  tposres3  48918  sepfsepc  48965  uptrlem1  49248  uptrlem2  49249  uptrlem3  49250  uptra  49253  uptrar  49254  uobeqw  49257  uptr2  49259  uptr2a  49260  fucoppcfunc  49450  aacllem  49839  amgmlemALT  49841