Theorem sstri 3940

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

This proof depends on syntax axioms:   ⊆ wss 3899

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 3916

This theorem is used by:  snsstp1  4777  snsstp2  4778  uniintsn  4945  elopabran  5536  ssrnres  6170  cossxp  6273  foimacnv  6840  ssimaex  6968  riotassuni  7415  oprabss  7526  dmexg  7911  rnexg  7912  mptmpoopabbrd  8092  fparlem3  8123  fparlem4  8124  snopsuppss  8189  tposssxp  8240  naddunif  8696  naddasslem1  8697  naddasslem2  8698  mapsspw  8899  sbthlem5  9103  sbthlem7  9105  cnvimamptfin  9335  marypha1lem  9418  ordtypelem4  9508  hartogslem1  9529  ttrclco  9712  cottrcl  9713  tc2  9734  frmin  9746  frrlem16  9755  tz9.12lem1  9787  rankval4  9877  rankxpl  9885  rankmapu  9888  rankxplim  9889  djuin  9992  infxpenlem  10085  ackbij1lem18  10307  cflm  10320  fin23lem29  10412  hsmexlem4  10500  hsmexlem5  10501  brdom3  10600  brdom5  10601  brdom4  10602  smobeth  10664  pwfseqlem3  10738  wundm  10806  wunrn  10807  wunex2  10816  ltsopi  10966  dmaddpi  10968  dmmulpi  10969  nqerf  11008  ltrelxr  11363  uzssre  12980  uzwo2  13032  infssuzle  13051  infssuzcl  13052  uzwo3  13063  nn0ssq  13077  nnssq  13078  qsscn  13080  rpnnen1lem3  13100  rpnnen1lem5  13102  dflt2  13270  ioosscn  13532  unitsscn  13624  fzval2  13635  fzssre  13652  fzossz  13807  fzossnn  13839  injresinj  13919  flval3  13948  uzsup  13996  uzrdgfni  14094  expcl2lem  14209  rpexpcl  14216  expge0  14234  expge1  14235  hashxrcl  14494  seqcoll  14602  xptrrel  15126  trclublem  15141  01sqrexlem3  15404  limsupval2  15640  limsupgre  15641  rlimpm  15660  rlimclim  15706  isercolllem1  15825  isercolllem2  15826  isercoll  15828  caurcvg  15837  caucvg  15839  summolem2a  15874  summolem2  15875  zsum  15877  fsumcvg3  15888  fsumrpcl  15896  fsumge0  15955  climfsum  15980  ackbijnn  15990  prodmolem2a  16094  prodmolem2  16095  zprod  16097  fprodrpcl  16116  fprodge0  16153  fprodge1  16155  rprisefaccl  16183  divalglem8  16563  sadaddlem  16629  lcmfval  16789  isprm3  16851  maxprmfct  16878  pclem  17009  prmreclem1  17087  prmreclem2  17088  prmreclem3  17089  1arith  17098  4sqlem11  17126  ramtlecl  17171  ramcl2lem  17180  ramxrcl  17188  prmgaplem3  17224  prmgaplem4  17225  cshwshashlem1  17266  structfn  17327  strleun  17328  ressbasss  17410  ressbasss2  17412  srngbase  17474  srngplusg  17475  srngmulr  17476  lmodbase  17490  lmodplusg  17491  lmodsca  17492  ipsbase  17501  ipsaddg  17502  ipsmulr  17503  ipssca  17504  ipsvsca  17505  ipsip  17506  phlbase  17511  phlplusg  17512  phlsca  17513  phlvsca  17514  phlip  17515  odrngbas  17568  odrngplusg  17569  odrngmulr  17570  odrngtset  17571  odrngle  17572  odrngds  17573  prdsvallem  17618  prdsval  17619  prdssca  17620  prdsbas  17621  prdsplusg  17622  prdsmulr  17623  prdsvsca  17624  prdsip  17625  prdsle  17626  prdsds  17628  prdstset  17630  prdshom  17631  prdsco  17632  imasbas  17677  imasds  17678  imasplusg  17682  imasmulr  17683  imassca  17684  imasvsca  17685  imasip  17686  imastset  17687  imasle  17688  wunfunc  18069  fullfunc  18076  fthfunc  18077  isfull  18080  isfth  18084  wunnat  18127  dmcoass  18234  catcisolem  18278  catciso  18279  catcoppccl  18285  catcfuccl  18286  catcxpccl  18374  ipobas  18698  ipolerval  18699  ipotset  18700  psdmrn  18740  psss  18747  ledm  18757  lern  18758  dirdm  18767  dirge  18770  mulgfval  19272  mvdco  19652  f1omvdconj  19653  gexex  20060  gsumval3  20114  lssacs  21235  cnfldbas  21675  mpocnfldadd  21676  mpocnfldmul  21678  cnfldcj  21680  cnfldtset  21681  cnfldle  21682  cnfldds  21683  cnfldunif  21684  rge0srg  21737  zntoslem  21855  asplss  22174  aspsubrg  22176  psrass1lem  22234  psrbas  22235  psrplusg  22238  psrmulr  22243  psrsca  22248  psrvscafval  22249  psrass1  22264  psrass23l  22267  psrcom  22268  psrass23  22269  psropprmul  22548  coe1mul2  22581  ofco2  22759  toponsspwpw  23233  dmtopon  23234  leordtval2  23523  lmbrf  23571  lmres  23611  fiuncmp  23715  comppfsc  23844  1stckgenlem  23865  kgencn3  23870  ptbasfi  23893  xkoopn  23901  txcnmpt  23936  txkgen  23964  opnfbas  24154  fmfnfmlem4  24269  tsmsxplem1  24465  trust  24541  restutop  24549  nmoffn  25023  nmofval  25026  nmogelb  25028  nmolb  25029  nmof  25031  qtopbas  25071  tgqioo  25112  re2ndc  25113  iitopon  25193  dfii3  25197  cnheiborlem  25268  bndth  25272  lebnumii  25280  pcoass  25338  cphsqrtcl  25498  lmmbrf  25576  iscauf  25594  caucfil  25597  lmclimf  25618  rrxmval  25719  rrxmet  25722  ovolfioo  25781  ovolficc  25782  ovolficcss  25783  ovolfsf  25785  ovollb  25793  ovolicc2lem3  25833  ovolicc2lem4  25834  ovolicc2  25836  volf  25843  volsup  25870  ovolfs2  25885  uniiccdif  25892  uniioovol  25893  uniiccvol  25894  uniioombllem2  25897  uniioombllem3a  25898  uniioombllem3  25899  uniioombllem4  25900  uniioombllem5  25901  uniioombl  25903  dyadmbllem  25913  dyadmbl  25914  opnmbllem  25915  opnmblALT  25917  volsup2  25919  vitalilem4  25925  vitalilem5  25926  vitali  25927  mbfimaopnlem  25969  mbflimsup  25980  i1f0  26001  i1f1  26004  itg11  26005  itg2mulc  26061  itg2gt0  26074  ellimc2  26190  limcresi  26198  dvreslem  26222  dvres2lem  26223  dvaddbr  26251  dvmulbr  26252  dvlipcn  26307  c1liplem1  26309  lhop1lem  26326  lhop1  26327  lhop2  26328  lhop  26329  dvfsumrlim  26344  ftc1cn  26356  itgsubstlem  26361  itgsubst  26362  itgpowd  26363  mdegleb  26375  mdeglt  26376  mdegldg  26377  mdegxrcl  26378  mdegcl  26380  mdegaddle  26385  mdegmullem  26389  deg1mul3le  26428  ig1peu  26486  ig1pdvds  26491  aacjcl  26647  aannenlem2  26649  aannenlem3  26650  aalioulem2  26653  taylfval  26679  radcnvcl  26737  radcnvlt1  26738  radcnvle  26740  abelth  26761  abelth2  26762  pilem2  26772  pilem3  26773  pige3ALT  26841  recosf1o  26856  resinf1o  26857  tanord1  26858  logcn  26968  dvlog  26972  dvlog2lem  26973  efopn  26979  logtayl  26981  cxpcn3  27069  loglesqrt  27082  ssscongptld  27143  leibpi  27263  efrlim  27290  jensenlem1  27307  jensenlem2  27308  jensen  27309  amgm  27311  lgamgulmlem2  27350  ftalem5  27397  efnnfsumcl  27423  efchtdvds  27479  mpodvdsmulf1o  27514  fsumdvdsmul  27515  dvdsmulf1o  27516  lgsfcl2  27623  2sqlem6  27743  2sqlem8  27746  2sqlem9  27747  rpvmasumlem  27807  rpvmasum2  27832  dchrisum0re  27833  dchrisum0lem3  27839  dchrisum0  27840  rplogsum  27847  dirith2  27848  noextendseq  28017  oldf  28216  leftssno  28252  rightssno  28253  addbdaylem  28396  mulsproplem12  28506  mulsproplem13  28507  mulsproplem14  28508  mulsasslem3  28544  precsexlem11  28596  oncutlt  28643  bdayons  28655  nnssno  28701  axtgcgrrflx  28917  axtgcgrid  28918  axtgsegcon  28919  axtg5seg  28920  axtgbtwnid  28921  axtgpasch  28922  axtgcont1  28923  tgcgr4  28987  motcgrg  29000  tglng  29002  upgrss  29659  pthdivtx  30305  disjxwwlkn  30495  ex-fpar  31056  nmlno0lem  31388  hlimcaui  31831  chsspwh  31842  shsss  31908  chintcli  31926  shsleji  31965  shub1i  31969  shsval2i  31982  lejdii  32133  spanuni  32139  sshhococi  32141  spansnpji  32173  osumcori  32238  5oai  32256  3oalem6  32262  3oai  32263  pjssmii  32276  mayete3i  32323  mayetes3i  32324  nmlnop0iALT  32590  imaelshi  32653  pjnmopi  32743  pjclem1  32790  pjci  32795  mdslmd1lem1  32920  shatomistici  32956  hatomistici  32957  chpssati  32958  xppreima  33232  iundisjfi  33381  iundisj2fi  33382  fprodex01  33409  indsumin  33421  xrsmulgzz  33563  fsumrp0cl  33575  gsummpt2co  33602  cycpmfv2  33668  cycpmrn  33697  rlocbas  33822  rlocaddval  33823  rlocmulval  33824  1fldgenq  33877  xrge0slmod  33902  lsmsnorb  33939  idlsrgbas  34029  idlsrgplusg  34030  idlsrgmulr  34032  idlsrgtset  34033  selvply1rhmlemb  34144  esplyind  34200  vietalem  34204  constrextdg2  34374  ordtconnlem1  34549  xrge0iifhom  34562  lmlimxrge0  34573  lmxrge0  34577  esumcst  34688  esumpfinvallem  34699  esumpfinval  34700  esumpfinvalf  34701  esumcvg  34711  imambfm  34887  elmbfmvol2  34892  sxbrsigalem3  34897  sxbrsigalem2  34911  sxbrsigalem4  34912  sitgclg  34967  eulerpartlem1  34992  eulerpartlemgvv  35001  eulerpartlemgh  35003  eulerpartlemgf  35004  ballotlemfc0  35118  ballotlemfcc  35119  ballotlemiex  35127  ballotlemsup  35130  ballotlemsima  35141  ballotlemrv2  35147  ballotth  35163  signsplypnf  35172  signsply0  35173  rpsqrtcn  35215  itgexpif  35228  fsum2dsub  35229  reprfi2  35245  chtvalz  35251  breprexplemc  35254  breprexpnat  35256  circlemeth  35262  circlemethnat  35263  circlevma  35264  circlemethhgt  35265  hgt750lemd  35270  hgt750lema  35279  tgoldbachgtde  35282  tgoldbachgtda  35283  tgoldbachgt  35285  bnj1145  35616  bnj1286  35642  subfacp1lem2a  35924  erdszelem4  35938  erdszelem5  35939  erdszelem7  35941  erdszelem8  35942  kur14lem7  35956  kur14lem9  35958  resconn  35990  iccllysconn  35994  txpss3v  36620  txprel  36621  limitssson  36653  finminlem  37086  tailf  37143  filnetlem3  37148  onint1  37217  ttcuniun  37278  bj-unrab  37819  bj-2upln1upl  37917  bj-imdirco  38091  bj-rvecssabl  38207  taupilem2  38223  taupi  38224  poimirlem3  38521  poimirlem30  38548  poimirlem31  38549  poimirlem32  38550  broucube  38552  opnmbllem0  38554  mblfinlem1  38555  mblfinlem2  38556  mblfinlem3  38557  mblfinlem4  38558  ismblfin  38559  mbfposadd  38565  cnambfre  38566  itg2addnc  38572  ftc1cnnclem  38589  ftc1cnnc  38590  ftc1anclem3  38593  ftc1anclem7  38597  ftc1anc  38599  ftc2nc  38600  dvreasin  38604  dvreacos  38605  areacirclem1  38606  areacirclem2  38607  areacirc  38611  caures  38674  reheibor  38753  xrnss3v  39293  xrnrel  39294  atlatmstc  40356  atlatle  40357  pmaple  40798  sspadd1  40852  sspadd2  40853  dvrelog2  43094  dvrelog3  43095  rpsscn  43336  sumcubes  43350  redvmptabs  43391  frlmnzcoordinf  43634  diophin  43762  4rexfrabdioph  43784  6rexfrabdioph  43785  irrapxlem1  43808  irrapx1  43814  rmxyelqirr  43896  monotuz  43927  jm2.27dlem5  43999  hbtlem2  44110  algbase  44160  algaddg  44161  algmulr  44162  algsca  44163  algvsca  44164  arearect  44201  areaquad  44202  rtrclex  44602  trclubgNEW  44603  trclexi  44605  rtrclexi  44606  cnvtrcl0  44611  dfrtrcl5  44614  trrelsuperrel2dg  44656  relexpaddss  44703  brtrclfv2  44712  frege131d  44749  xphe  44766  clsk3nimkb  45025  gneispace  45119  k0004val0  45139  inaex  45266  lhe4.4ex1a  45298  uzmptshftfval  45315  binomcxplemdvbinom  45322  binomcxplemcvg  45323  binomcxplemnotnn0  45325  relopabVD  45868  dmwf  45933  rnwf  45934  hfdm  45996  hfrn  45997  fzisoeu  46285  fzsscn  46296  fzossuz  46361  zssxr  46377  uzssre2  46386  supminfxr  46443  uzsscn  46454  rpssxr  46459  uzinico  46540  limcresiooub  46621  limcresioolb  46622  limcleqr  46623  limclner  46630  limclr  46634  limsupequzmpt2  46697  liminfval2  46747  liminfequzmpt2  46770  icccncfext  46866  cncficcgt0  46867  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  dvnprodlem2  46926  itgsin0pilem1  46929  itgsinexplem1  46933  itgsinexp  46934  dirkercncflem2  47083  fourierdlem16  47102  fourierdlem18  47104  fourierdlem20  47106  fourierdlem21  47107  fourierdlem22  47108  fourierdlem25  47111  fourierdlem37  47123  fourierdlem42  47128  fourierdlem50  47135  fourierdlem52  47137  fourierdlem62  47147  fourierdlem64  47149  fourierdlem66  47151  fourierdlem68  47153  fourierdlem74  47159  fourierdlem75  47160  fourierdlem76  47161  fourierdlem79  47164  fourierdlem83  47168  fourierdlem95  47180  fourierdlem101  47186  fourierdlem102  47187  fourierdlem103  47188  fourierdlem104  47189  fourierdlem112  47197  fourierdlem114  47199  sqwvfoura  47207  sqwvfourb  47208  fouriersw  47210  etransclem24  47237  etransclem48  47261  sge0sn  47358  sge0tsms  47359  sge0f1o  47361  sge0pr  47373  sge0resplit  47385  sge0split  47388  sge0iunmptlemre  47394  sge0isummpt2  47411  carageniuncllem1  47500  hoicvr  47527  hoicvrrex  47535  hoidmvlelem2  47575  hspmbl  47608  smfmullem4  47773  chnsuslle  47860  lamberte  47907  rehalfge1  48378  prmdvdsfmtnof1lem1  48638  prmdvdsfmtnof  48640  upgrimpthslem2  48975  upgrimpths  48976  oddibas  49239  2zrngbas  49308  2zrng0  49310  dmtposss  49953  tposres3  49958  sepfsepc  50005  uptrlem1  50287  uptrlem2  50288  uptrlem3  50289  uptra  50292  uptrar  50293  uobeqw  50296  uptr2  50298  uptr2a  50299  fucoppcfunc  50489  aacllem  50908  amgmlemALT  50957