Theorem sstri 3922

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 3920	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
4	1, 2, 3	mp2 9	1 ⊢ 𝐴 ⊆ 𝐶

This proof depends on syntax axioms:   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ss 3901

This theorem is used by:  snsstp1  4775  snsstp2  4776  uniintsn  4948  elopabran  5541  relopabi  5807  ssrnres  6186  cossxp  6296  foimacnv  6870  ssimaex  6999  riotassuni  7446  oprabss  7557  dmexg  7945  rnexg  7946  mptmpoopabbrd  8127  fparlem3  8160  fparlem4  8161  snopsuppss  8232  tposssxp  8283  naddunif  8739  naddasslem1  8740  naddasslem2  8741  mapsspw  8942  sbthlem5  9146  sbthlem7  9148  cnvimamptfin  9378  marypha1lem  9460  ordtypelem4  9550  hartogslem1  9571  ttrclco  9754  cottrcl  9755  tc2  9776  frmin  9788  frrlem16  9797  tz9.12lem1  9829  rankval4  9919  rankxpl  9927  rankmapu  9930  rankxplim  9931  djuin  10034  infxpenlem  10129  ackbij1lem18  10351  cflm  10364  fin23lem29  10456  hsmexlem4  10544  hsmexlem5  10545  brdom3  10644  brdom5  10645  brdom4  10646  smobeth  10708  pwfseqlem3  10782  wundm  10850  wunrn  10851  wunex2  10860  ltsopi  11010  dmaddpi  11012  dmmulpi  11013  nqerf  11052  ltrelxr  11407  uzssre  13025  uzwo2  13077  infssuzle  13096  infssuzcl  13097  uzwo3  13108  nn0ssq  13122  nnssq  13123  qsscn  13125  rpnnen1lem3  13145  rpnnen1lem5  13147  dflt2  13315  ioosscn  13577  unitsscn  13669  fzval2  13680  fzssre  13697  fzossz  13852  fzossnn  13884  injresinj  13964  flval3  13993  uzsup  14041  uzrdgfni  14139  expcl2lem  14254  rpexpcl  14261  expge0  14279  expge1  14280  hashxrcl  14540  seqcoll  14648  xptrrel  15174  trclublem  15189  01sqrexlem3  15452  limsupval2  15688  limsupgre  15689  rlimpm  15708  rlimclim  15754  isercolllem1  15873  isercolllem2  15874  isercoll  15876  caurcvg  15885  caucvg  15887  summolem2a  15922  summolem2  15923  zsum  15925  fsumcvg3  15936  fsumrpcl  15944  fsumge0  16003  climfsum  16028  ackbijnn  16038  prodmolem2a  16142  prodmolem2  16143  zprod  16145  fprodrpcl  16164  fprodge0  16201  fprodge1  16203  rprisefaccl  16231  divalglem8  16611  sadaddlem  16677  lcmfval  16837  isprm3  16899  maxprmfct  16926  pclem  17057  prmreclem1  17135  prmreclem2  17136  prmreclem3  17137  1arith  17146  4sqlem11  17174  ramtlecl  17219  ramcl2lem  17228  ramxrcl  17236  prmgaplem3  17272  prmgaplem4  17273  cshwshashlem1  17314  structfn  17375  strleun  17376  ressbasss  17458  ressbasss2  17460  srngbase  17522  srngplusg  17523  srngmulr  17524  lmodbase  17538  lmodplusg  17539  lmodsca  17540  ipsbase  17549  ipsaddg  17550  ipsmulr  17551  ipssca  17552  ipsvsca  17553  ipsip  17554  phlbase  17559  phlplusg  17560  phlsca  17561  phlvsca  17562  phlip  17563  odrngbas  17616  odrngplusg  17617  odrngmulr  17618  odrngtset  17619  odrngle  17620  odrngds  17621  prdsvallem  17666  prdsval  17667  prdssca  17668  prdsbas  17669  prdsplusg  17670  prdsmulr  17671  prdsvsca  17672  prdsip  17673  prdsle  17674  prdsds  17676  prdstset  17678  prdshom  17679  prdsco  17680  imasbas  17725  imasds  17726  imasplusg  17730  imasmulr  17731  imassca  17732  imasvsca  17733  imasip  17734  imastset  17735  imasle  17736  wunfunc  18117  fullfunc  18124  fthfunc  18125  isfull  18128  isfth  18132  wunnat  18175  dmcoass  18282  catcisolem  18326  catciso  18327  catcoppccl  18333  catcfuccl  18334  catcxpccl  18422  ipobas  18746  ipolerval  18747  ipotset  18748  psdmrn  18788  psss  18795  ledm  18805  lern  18806  dirdm  18815  dirge  18818  mulgfval  19320  mvdco  19701  f1omvdconj  19702  gexex  20109  gsumval3  20163  lssacs  21284  cnfldbas  21724  mpocnfldadd  21725  mpocnfldmul  21727  cnfldcj  21729  cnfldtset  21730  cnfldle  21731  cnfldds  21732  cnfldunif  21733  rge0srg  21788  zntoslem  21906  asplss  22225  aspsubrg  22227  psrass1lem  22285  psrbas  22286  psrplusg  22289  psrmulr  22294  psrsca  22299  psrvscafval  22300  psrass1  22315  psrass23l  22318  psrcom  22319  psrass23  22320  psropprmul  22599  coe1mul2  22632  ofco2  22810  toponsspwpw  23284  dmtopon  23285  leordtval2  23574  lmbrf  23622  lmres  23662  fiuncmp  23766  comppfsc  23895  1stckgenlem  23916  kgencn3  23921  ptbasfi  23944  xkoopn  23952  txcnmpt  23987  txkgen  24015  opnfbas  24205  fmfnfmlem4  24320  tsmsxplem1  24516  trust  24592  restutop  24600  nmoffn  25074  nmofval  25077  nmogelb  25079  nmolb  25080  nmof  25082  qtopbas  25122  tgqioo  25163  re2ndc  25164  cnheiborlem  25319  bndth  25323  lebnumii  25331  pcoass  25389  cphsqrtcl  25549  lmmbrf  25627  iscauf  25645  caucfil  25648  lmclimf  25669  rrxmval  25770  rrxmet  25773  ovolfioo  25832  ovolficc  25833  ovolficcss  25834  ovolfsf  25836  ovollb  25844  ovolicc2lem3  25884  ovolicc2lem4  25885  ovolicc2  25887  volf  25894  volsup  25921  ovolfs2  25936  uniiccdif  25943  uniioovol  25944  uniiccvol  25945  uniioombllem2  25948  uniioombllem3a  25949  uniioombllem3  25950  uniioombllem4  25951  uniioombllem5  25952  uniioombl  25954  dyadmbllem  25964  dyadmbl  25965  opnmbllem  25966  opnmblALT  25968  volsup2  25970  vitalilem4  25976  vitalilem5  25977  vitali  25978  mbfimaopnlem  26020  mbflimsup  26031  i1f0  26052  i1f1  26055  itg11  26056  itg2mulc  26112  itg2gt0  26125  ellimc2  26241  limcresi  26249  dvreslem  26273  dvres2lem  26274  dvaddbr  26302  dvmulbr  26303  dvlipcn  26358  c1liplem1  26360  lhop1lem  26377  lhop1  26378  lhop2  26379  lhop  26380  dvfsumrlim  26395  ftc1cn  26407  itgsubstlem  26412  itgsubst  26413  itgpowd  26414  mdegleb  26426  mdeglt  26427  mdegldg  26428  mdegxrcl  26429  mdegcl  26431  mdegaddle  26436  mdegmullem  26440  deg1mul3le  26479  ig1peu  26537  ig1pdvds  26542  aacjcl  26700  aannenlem2  26702  aannenlem3  26703  aalioulem2  26706  taylfval  26732  radcnvcl  26790  radcnvlt1  26791  radcnvle  26793  abelth  26814  abelth2  26815  pilem2  26825  pilem3  26826  pige3ALT  26894  recosf1o  26909  resinf1o  26910  tanord1  26911  logcn  27021  dvlog  27025  dvlog2lem  27026  efopn  27032  logtayl  27034  cxpcn3  27122  loglesqrt  27135  ssscongptld  27196  leibpi  27316  efrlim  27343  jensenlem1  27360  jensenlem2  27361  jensen  27362  amgm  27364  lgamgulmlem2  27403  ftalem5  27450  efnnfsumcl  27476  efchtdvds  27532  mpodvdsmulf1o  27567  fsumdvdsmul  27568  dvdsmulf1o  27569  lgsfcl2  27676  2sqlem6  27796  2sqlem8  27799  2sqlem9  27800  rpvmasumlem  27860  rpvmasum2  27885  dchrisum0re  27886  dchrisum0lem3  27892  dchrisum0  27893  rplogsum  27900  dirith2  27901  noextendseq  28070  oldf  28269  leftssno  28305  rightssno  28306  addbdaylem  28449  mulsproplem12  28559  mulsproplem13  28560  mulsproplem14  28561  mulsasslem3  28597  precsexlem11  28649  oncutlt  28696  bdayons  28708  nnssno  28754  axtgcgrrflx  28970  axtgcgrid  28971  axtgsegcon  28972  axtg5seg  28973  axtgbtwnid  28974  axtgpasch  28975  axtgcont1  28976  tgcgr4  29040  motcgrg  29053  tglng  29055  upgrss  29712  pthdivtx  30358  disjxwwlkn  30548  ex-fpar  31109  nmlno0lem  31441  hlimcaui  31884  chsspwh  31895  shsss  31961  chintcli  31979  shsleji  32018  shub1i  32022  shsval2i  32035  lejdii  32186  spanuni  32192  sshhococi  32194  spansnpji  32226  osumcori  32291  5oai  32309  3oalem6  32315  3oai  32316  pjssmii  32329  mayete3i  32376  mayetes3i  32377  nmlnop0iALT  32643  imaelshi  32706  pjnmopi  32796  pjclem1  32843  pjci  32848  mdslmd1lem1  32973  shatomistici  33009  hatomistici  33010  chpssati  33011  xppreima  33327  iundisjfi  33474  iundisj2fi  33475  fprodex01  33502  indsumin  33514  xrsmulgzz  33659  fsumrp0cl  33671  gsummpt2co  33698  cycpmfv2  33764  cycpmrn  33793  rlocbas  33918  rlocaddval  33919  rlocmulval  33920  1fldgenq  33981  xrge0slmod  34006  lsmsnorb  34043  idlsrgbas  34133  idlsrgplusg  34134  idlsrgmulr  34136  idlsrgtset  34137  selvply1rhmlemb  34255  esplyind  34311  vietalem  34315  constrextdg2  34485  ordtconnlem1  34660  xrge0iifhom  34673  lmlimxrge0  34684  lmxrge0  34688  esumcst  34799  esumpfinvallem  34810  esumpfinval  34811  esumpfinvalf  34812  esumcvg  34822  imambfm  34998  elmbfmvol2  35003  sxbrsigalem3  35008  sxbrsigalem2  35022  sxbrsigalem4  35023  sitgclg  35078  eulerpartlem1  35103  eulerpartlemgvv  35112  eulerpartlemgh  35114  eulerpartlemgf  35115  ballotlemfc0  35229  ballotlemfcc  35230  ballotlemiex  35238  ballotlemsup  35241  ballotlemsima  35252  ballotlemrv2  35258  ballotth  35274  signsplypnf  35283  signsply0  35284  rpsqrtcn  35326  itgexpif  35339  fsum2dsub  35340  reprfi2  35356  chtvalz  35362  breprexplemc  35365  breprexpnat  35367  circlemeth  35373  circlemethnat  35374  circlevma  35375  circlemethhgt  35376  hgt750lemd  35381  hgt750lema  35390  tgoldbachgtde  35393  tgoldbachgtda  35394  tgoldbachgt  35396  bnj1145  35727  bnj1286  35753  abweex  35835  j0ltalephlem  36041  subfacp1lem2a  36146  erdszelem4  36160  erdszelem5  36161  erdszelem7  36163  erdszelem8  36164  kur14lem7  36178  kur14lem9  36180  resconn  36212  iccllysconn  36216  txpss3v  36848  txprel  36849  limitssson  36881  finminlem  37314  tailf  37371  filnetlem3  37376  onint1  37445  ttcuniun  37506  bj-unrab  38047  bj-2upln1upl  38145  bj-imdirco  38372  bj-rvecssabl  38488  taupilem2  38504  taupi  38505  poimirlem3  38802  poimirlem30  38829  poimirlem31  38830  poimirlem32  38831  broucube  38833  opnmbllem0  38835  mblfinlem1  38836  mblfinlem2  38837  mblfinlem3  38838  mblfinlem4  38839  ismblfin  38840  mbfposadd  38846  cnambfre  38847  itg2addnc  38853  ftc1cnnclem  38870  ftc1cnnc  38871  ftc1anclem3  38874  ftc1anclem7  38878  ftc1anc  38880  ftc2nc  38881  dvreasin  38885  dvreacos  38886  areacirclem1  38887  areacirclem2  38888  areacirc  38892  caures  38953  reheibor  39032  xrnss3v  39572  xrnrel  39573  atlatmstc  40635  atlatle  40636  pmaple  41077  sspadd1  41131  sspadd2  41132  dvrelog2  43373  dvrelog3  43374  rpsscn  43616  sumcubes  43630  redvmptabs  43671  frlmnzcoordinf  43914  diophin  44043  4rexfrabdioph  44065  6rexfrabdioph  44066  irrapxlem1  44089  irrapx1  44095  rmxyelqirr  44177  monotuz  44208  jm2.27dlem5  44280  hbtlem2  44385  algbase  44431  algaddg  44432  algmulr  44433  algsca  44434  algvsca  44435  arearect  44472  areaquad  44473  rtrclex  44872  trclubgNEW  44873  trclexi  44875  rtrclexi  44876  cnvtrcl0  44881  dfrtrcl5  44884  trrelsuperrel2dg  44926  relexpaddss  44973  brtrclfv2  44982  frege131d  45019  xphe  45036  clsk3nimkb  45295  gneispace  45389  inaex  45536  lhe4.4ex1a  45568  uzmptshftfval  45585  binomcxplemdvbinom  45592  binomcxplemcvg  45593  binomcxplemnotnn0  45595  relopabVD  46137  dmwf  46213  rnwf  46214  hfdm  46276  hfrn  46277  hfstructhf  46291  fzisoeu  46583  fzsscn  46594  fzossuz  46659  zssxr  46675  uzssre2  46684  supminfxr  46741  uzsscn  46752  rpssxr  46757  uzinico  46838  limcresiooub  46919  limcresioolb  46920  limcleqr  46921  limclner  46928  limclr  46932  limsupequzmpt2  46995  liminfval2  47045  liminfequzmpt2  47068  icccncfext  47164  cncficcgt0  47165  ioodvbdlimc1lem2  47209  ioodvbdlimc2lem  47211  dvnprodlem2  47224  itgsin0pilem1  47227  itgsinexplem1  47231  itgsinexp  47232  dirkercncflem2  47381  fourierdlem16  47400  fourierdlem18  47402  fourierdlem20  47404  fourierdlem21  47405  fourierdlem22  47406  fourierdlem25  47409  fourierdlem37  47421  fourierdlem42  47426  fourierdlem50  47433  fourierdlem52  47435  fourierdlem62  47445  fourierdlem64  47447  fourierdlem66  47449  fourierdlem68  47451  fourierdlem74  47457  fourierdlem75  47458  fourierdlem76  47459  fourierdlem79  47462  fourierdlem83  47466  fourierdlem95  47478  fourierdlem101  47484  fourierdlem102  47485  fourierdlem103  47486  fourierdlem104  47487  fourierdlem112  47495  fourierdlem114  47497  sqwvfoura  47505  sqwvfourb  47506  fouriersw  47508  etransclem24  47535  etransclem48  47559  sge0sn  47656  sge0tsms  47657  sge0f1o  47659  sge0pr  47671  sge0resplit  47683  sge0split  47686  sge0iunmptlemre  47692  sge0isummpt2  47709  carageniuncllem1  47798  hoicvr  47825  hoicvrrex  47833  hoidmvlelem2  47873  hspmbl  47906  smfmullem4  48071  chnsuslle  48158  lamberte  48205  rehalfge1  48676  prmdvdsfmtnof1lem1  48936  prmdvdsfmtnof  48938  upgrimpthslem2  49273  upgrimpths  49274  oddibas  49537  2zrngbas  49606  2zrng0  49608  dmtposss  50314  tposres3  50319  sepfsepc  50367  uptrlem1  50651  uptrlem2  50652  uptrlem3  50653  uptra  50656  uptrar  50657  uobeqw  50660  uptr2  50662  uptr2a  50663  fucoppcfunc  50872  parhomssun  51072  aacllem  51361  amgmlemALT  51410