Theorem sstri 3917

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

This proof depends on syntax axioms:   ⊆ wss 3895

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

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

This theorem is used by:  snsstp1  4771  snsstp2  4772  uniintsn  4944  elopabran  5535  ssrnres  6169  cossxp  6274  foimacnv  6843  ssimaex  6971  riotassuni  7418  oprabss  7529  dmexg  7914  rnexg  7915  mptmpoopabbrd  8095  fparlem3  8128  fparlem4  8129  snopsuppss  8200  tposssxp  8251  naddunif  8707  naddasslem1  8708  naddasslem2  8709  mapsspw  8910  sbthlem5  9114  sbthlem7  9116  cnvimamptfin  9346  marypha1lem  9429  ordtypelem4  9519  hartogslem1  9540  ttrclco  9723  cottrcl  9724  tc2  9745  frmin  9757  frrlem16  9766  tz9.12lem1  9798  rankval4  9888  rankxpl  9896  rankmapu  9899  rankxplim  9900  djuin  10003  infxpenlem  10096  ackbij1lem18  10318  cflm  10331  fin23lem29  10423  hsmexlem4  10511  hsmexlem5  10512  brdom3  10611  brdom5  10612  brdom4  10613  smobeth  10675  pwfseqlem3  10749  wundm  10817  wunrn  10818  wunex2  10827  ltsopi  10977  dmaddpi  10979  dmmulpi  10980  nqerf  11019  ltrelxr  11374  uzssre  12991  uzwo2  13043  infssuzle  13062  infssuzcl  13063  uzwo3  13074  nn0ssq  13088  nnssq  13089  qsscn  13091  rpnnen1lem3  13111  rpnnen1lem5  13113  dflt2  13281  ioosscn  13543  unitsscn  13635  fzval2  13646  fzssre  13663  fzossz  13818  fzossnn  13850  injresinj  13930  flval3  13959  uzsup  14007  uzrdgfni  14105  expcl2lem  14220  rpexpcl  14227  expge0  14245  expge1  14246  hashxrcl  14505  seqcoll  14613  xptrrel  15139  trclublem  15154  01sqrexlem3  15417  limsupval2  15653  limsupgre  15654  rlimpm  15673  rlimclim  15719  isercolllem1  15838  isercolllem2  15839  isercoll  15841  caurcvg  15850  caucvg  15852  summolem2a  15887  summolem2  15888  zsum  15890  fsumcvg3  15901  fsumrpcl  15909  fsumge0  15968  climfsum  15993  ackbijnn  16003  prodmolem2a  16107  prodmolem2  16108  zprod  16110  fprodrpcl  16129  fprodge0  16166  fprodge1  16168  rprisefaccl  16196  divalglem8  16576  sadaddlem  16642  lcmfval  16802  isprm3  16864  maxprmfct  16891  pclem  17022  prmreclem1  17100  prmreclem2  17101  prmreclem3  17102  1arith  17111  4sqlem11  17139  ramtlecl  17184  ramcl2lem  17193  ramxrcl  17201  prmgaplem3  17237  prmgaplem4  17238  cshwshashlem1  17279  structfn  17340  strleun  17341  ressbasss  17423  ressbasss2  17425  srngbase  17487  srngplusg  17488  srngmulr  17489  lmodbase  17503  lmodplusg  17504  lmodsca  17505  ipsbase  17514  ipsaddg  17515  ipsmulr  17516  ipssca  17517  ipsvsca  17518  ipsip  17519  phlbase  17524  phlplusg  17525  phlsca  17526  phlvsca  17527  phlip  17528  odrngbas  17581  odrngplusg  17582  odrngmulr  17583  odrngtset  17584  odrngle  17585  odrngds  17586  prdsvallem  17631  prdsval  17632  prdssca  17633  prdsbas  17634  prdsplusg  17635  prdsmulr  17636  prdsvsca  17637  prdsip  17638  prdsle  17639  prdsds  17641  prdstset  17643  prdshom  17644  prdsco  17645  imasbas  17690  imasds  17691  imasplusg  17695  imasmulr  17696  imassca  17697  imasvsca  17698  imasip  17699  imastset  17700  imasle  17701  wunfunc  18082  fullfunc  18089  fthfunc  18090  isfull  18093  isfth  18097  wunnat  18140  dmcoass  18247  catcisolem  18291  catciso  18292  catcoppccl  18298  catcfuccl  18299  catcxpccl  18387  ipobas  18711  ipolerval  18712  ipotset  18713  psdmrn  18753  psss  18760  ledm  18770  lern  18771  dirdm  18780  dirge  18783  mulgfval  19285  mvdco  19665  f1omvdconj  19666  gexex  20073  gsumval3  20127  lssacs  21248  cnfldbas  21688  mpocnfldadd  21689  mpocnfldmul  21691  cnfldcj  21693  cnfldtset  21694  cnfldle  21695  cnfldds  21696  cnfldunif  21697  rge0srg  21750  zntoslem  21868  asplss  22187  aspsubrg  22189  psrass1lem  22247  psrbas  22248  psrplusg  22251  psrmulr  22256  psrsca  22261  psrvscafval  22262  psrass1  22277  psrass23l  22280  psrcom  22281  psrass23  22282  psropprmul  22561  coe1mul2  22594  ofco2  22772  toponsspwpw  23246  dmtopon  23247  leordtval2  23536  lmbrf  23584  lmres  23624  fiuncmp  23728  comppfsc  23857  1stckgenlem  23878  kgencn3  23883  ptbasfi  23906  xkoopn  23914  txcnmpt  23949  txkgen  23977  opnfbas  24167  fmfnfmlem4  24282  tsmsxplem1  24478  trust  24554  restutop  24562  nmoffn  25036  nmofval  25039  nmogelb  25041  nmolb  25042  nmof  25044  qtopbas  25084  tgqioo  25125  re2ndc  25126  cnheiborlem  25281  bndth  25285  lebnumii  25293  pcoass  25351  cphsqrtcl  25511  lmmbrf  25589  iscauf  25607  caucfil  25610  lmclimf  25631  rrxmval  25732  rrxmet  25735  ovolfioo  25794  ovolficc  25795  ovolficcss  25796  ovolfsf  25798  ovollb  25806  ovolicc2lem3  25846  ovolicc2lem4  25847  ovolicc2  25849  volf  25856  volsup  25883  ovolfs2  25898  uniiccdif  25905  uniioovol  25906  uniiccvol  25907  uniioombllem2  25910  uniioombllem3a  25911  uniioombllem3  25912  uniioombllem4  25913  uniioombllem5  25914  uniioombl  25916  dyadmbllem  25926  dyadmbl  25927  opnmbllem  25928  opnmblALT  25930  volsup2  25932  vitalilem4  25938  vitalilem5  25939  vitali  25940  mbfimaopnlem  25982  mbflimsup  25993  i1f0  26014  i1f1  26017  itg11  26018  itg2mulc  26074  itg2gt0  26087  ellimc2  26203  limcresi  26211  dvreslem  26235  dvres2lem  26236  dvaddbr  26264  dvmulbr  26265  dvlipcn  26320  c1liplem1  26322  lhop1lem  26339  lhop1  26340  lhop2  26341  lhop  26342  dvfsumrlim  26357  ftc1cn  26369  itgsubstlem  26374  itgsubst  26375  itgpowd  26376  mdegleb  26388  mdeglt  26389  mdegldg  26390  mdegxrcl  26391  mdegcl  26393  mdegaddle  26398  mdegmullem  26402  deg1mul3le  26441  ig1peu  26499  ig1pdvds  26504  aacjcl  26660  aannenlem2  26662  aannenlem3  26663  aalioulem2  26666  taylfval  26692  radcnvcl  26750  radcnvlt1  26751  radcnvle  26753  abelth  26774  abelth2  26775  pilem2  26785  pilem3  26786  pige3ALT  26854  recosf1o  26869  resinf1o  26870  tanord1  26871  logcn  26981  dvlog  26985  dvlog2lem  26986  efopn  26992  logtayl  26994  cxpcn3  27082  loglesqrt  27095  ssscongptld  27156  leibpi  27276  efrlim  27303  jensenlem1  27320  jensenlem2  27321  jensen  27322  amgm  27324  lgamgulmlem2  27363  ftalem5  27410  efnnfsumcl  27436  efchtdvds  27492  mpodvdsmulf1o  27527  fsumdvdsmul  27528  dvdsmulf1o  27529  lgsfcl2  27636  2sqlem6  27756  2sqlem8  27759  2sqlem9  27760  rpvmasumlem  27820  rpvmasum2  27845  dchrisum0re  27846  dchrisum0lem3  27852  dchrisum0  27853  rplogsum  27860  dirith2  27861  noextendseq  28030  oldf  28229  leftssno  28265  rightssno  28266  addbdaylem  28409  mulsproplem12  28519  mulsproplem13  28520  mulsproplem14  28521  mulsasslem3  28557  precsexlem11  28609  oncutlt  28656  bdayons  28668  nnssno  28714  axtgcgrrflx  28930  axtgcgrid  28931  axtgsegcon  28932  axtg5seg  28933  axtgbtwnid  28934  axtgpasch  28935  axtgcont1  28936  tgcgr4  29000  motcgrg  29013  tglng  29015  upgrss  29672  pthdivtx  30318  disjxwwlkn  30508  ex-fpar  31069  nmlno0lem  31401  hlimcaui  31844  chsspwh  31855  shsss  31921  chintcli  31939  shsleji  31978  shub1i  31982  shsval2i  31995  lejdii  32146  spanuni  32152  sshhococi  32154  spansnpji  32186  osumcori  32251  5oai  32269  3oalem6  32275  3oai  32276  pjssmii  32289  mayete3i  32336  mayetes3i  32337  nmlnop0iALT  32603  imaelshi  32666  pjnmopi  32756  pjclem1  32803  pjci  32808  mdslmd1lem1  32933  shatomistici  32969  hatomistici  32970  chpssati  32971  xppreima  33287  iundisjfi  33435  iundisj2fi  33436  fprodex01  33463  indsumin  33475  xrsmulgzz  33617  fsumrp0cl  33629  gsummpt2co  33656  cycpmfv2  33722  cycpmrn  33751  rlocbas  33876  rlocaddval  33877  rlocmulval  33878  1fldgenq  33931  xrge0slmod  33956  lsmsnorb  33993  idlsrgbas  34083  idlsrgplusg  34084  idlsrgmulr  34086  idlsrgtset  34087  selvply1rhmlemb  34198  esplyind  34254  vietalem  34258  constrextdg2  34428  ordtconnlem1  34603  xrge0iifhom  34616  lmlimxrge0  34627  lmxrge0  34631  esumcst  34742  esumpfinvallem  34753  esumpfinval  34754  esumpfinvalf  34755  esumcvg  34765  imambfm  34941  elmbfmvol2  34946  sxbrsigalem3  34951  sxbrsigalem2  34965  sxbrsigalem4  34966  sitgclg  35021  eulerpartlem1  35046  eulerpartlemgvv  35055  eulerpartlemgh  35057  eulerpartlemgf  35058  ballotlemfc0  35172  ballotlemfcc  35173  ballotlemiex  35181  ballotlemsup  35184  ballotlemsima  35195  ballotlemrv2  35201  ballotth  35217  signsplypnf  35226  signsply0  35227  rpsqrtcn  35269  itgexpif  35282  fsum2dsub  35283  reprfi2  35299  chtvalz  35305  breprexplemc  35308  breprexpnat  35310  circlemeth  35316  circlemethnat  35317  circlevma  35318  circlemethhgt  35319  hgt750lemd  35324  hgt750lema  35333  tgoldbachgtde  35336  tgoldbachgtda  35337  tgoldbachgt  35339  bnj1145  35670  bnj1286  35696  abweex  35770  j0ltalephlem  35947  subfacp1lem2a  36032  erdszelem4  36046  erdszelem5  36047  erdszelem7  36049  erdszelem8  36050  kur14lem7  36064  kur14lem9  36066  resconn  36098  iccllysconn  36102  txpss3v  36733  txprel  36734  limitssson  36766  finminlem  37199  tailf  37256  filnetlem3  37261  onint1  37330  ttcuniun  37391  bj-unrab  37932  bj-2upln1upl  38030  bj-imdirco  38205  bj-rvecssabl  38321  taupilem2  38337  taupi  38338  poimirlem3  38635  poimirlem30  38662  poimirlem31  38663  poimirlem32  38664  broucube  38666  opnmbllem0  38668  mblfinlem1  38669  mblfinlem2  38670  mblfinlem3  38671  mblfinlem4  38672  ismblfin  38673  mbfposadd  38679  cnambfre  38680  itg2addnc  38686  ftc1cnnclem  38703  ftc1cnnc  38704  ftc1anclem3  38707  ftc1anclem7  38711  ftc1anc  38713  ftc2nc  38714  dvreasin  38718  dvreacos  38719  areacirclem1  38720  areacirclem2  38721  areacirc  38725  caures  38788  reheibor  38867  xrnss3v  39407  xrnrel  39408  atlatmstc  40470  atlatle  40471  pmaple  40912  sspadd1  40966  sspadd2  40967  dvrelog2  43208  dvrelog3  43209  rpsscn  43450  sumcubes  43464  redvmptabs  43505  frlmnzcoordinf  43748  diophin  43877  4rexfrabdioph  43899  6rexfrabdioph  43900  irrapxlem1  43923  irrapx1  43929  rmxyelqirr  44011  monotuz  44042  jm2.27dlem5  44114  hbtlem2  44220  algbase  44270  algaddg  44271  algmulr  44272  algsca  44273  algvsca  44274  arearect  44311  areaquad  44312  rtrclex  44711  trclubgNEW  44712  trclexi  44714  rtrclexi  44715  cnvtrcl0  44720  dfrtrcl5  44723  trrelsuperrel2dg  44765  relexpaddss  44812  brtrclfv2  44821  frege131d  44858  xphe  44875  clsk3nimkb  45134  gneispace  45228  inaex  45375  lhe4.4ex1a  45407  uzmptshftfval  45424  binomcxplemdvbinom  45431  binomcxplemcvg  45432  binomcxplemnotnn0  45434  relopabVD  45977  dmwf  46049  rnwf  46050  hfdm  46112  hfrn  46113  hfstructhf  46124  fzisoeu  46410  fzsscn  46421  fzossuz  46486  zssxr  46502  uzssre2  46511  supminfxr  46568  uzsscn  46579  rpssxr  46584  uzinico  46665  limcresiooub  46746  limcresioolb  46747  limcleqr  46748  limclner  46755  limclr  46759  limsupequzmpt2  46822  liminfval2  46872  liminfequzmpt2  46895  icccncfext  46991  cncficcgt0  46992  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  dvnprodlem2  47051  itgsin0pilem1  47054  itgsinexplem1  47058  itgsinexp  47059  dirkercncflem2  47208  fourierdlem16  47227  fourierdlem18  47229  fourierdlem20  47231  fourierdlem21  47232  fourierdlem22  47233  fourierdlem25  47236  fourierdlem37  47248  fourierdlem42  47253  fourierdlem50  47260  fourierdlem52  47262  fourierdlem62  47272  fourierdlem64  47274  fourierdlem66  47276  fourierdlem68  47278  fourierdlem74  47284  fourierdlem75  47285  fourierdlem76  47286  fourierdlem79  47289  fourierdlem83  47293  fourierdlem95  47305  fourierdlem101  47311  fourierdlem102  47312  fourierdlem103  47313  fourierdlem104  47314  fourierdlem112  47322  fourierdlem114  47324  sqwvfoura  47332  sqwvfourb  47333  fouriersw  47335  etransclem24  47362  etransclem48  47386  sge0sn  47483  sge0tsms  47484  sge0f1o  47486  sge0pr  47498  sge0resplit  47510  sge0split  47513  sge0iunmptlemre  47519  sge0isummpt2  47536  carageniuncllem1  47625  hoicvr  47652  hoicvrrex  47660  hoidmvlelem2  47700  hspmbl  47733  smfmullem4  47898  chnsuslle  47985  lamberte  48032  rehalfge1  48503  prmdvdsfmtnof1lem1  48763  prmdvdsfmtnof  48765  upgrimpthslem2  49100  upgrimpths  49101  oddibas  49364  2zrngbas  49433  2zrng0  49435  dmtposss  50083  tposres3  50088  sepfsepc  50136  uptrlem1  50420  uptrlem2  50421  uptrlem3  50422  uptra  50425  uptrar  50426  uobeqw  50429  uptr2  50431  uptr2a  50432  fucoppcfunc  50641  parhomssun  50841  aacllem  51108  amgmlemALT  51157