Theorem sstri 3257

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

This proof depends on syntax axioms:   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  difdif2ss  3488  difdifdirss  3612  snsstp1  3865  snsstp2  3866  elopabran  4428  nnregexmid  4770  dmexg  5048  rnexg  5049  ssrnres  5233  cossxp  5313  cocnvss  5316  funinsn  5433  fabexg  5582  foimacnv  5660  ssimaex  5767  oprabss  6177  tposssxp  6524  mapsspw  6969  sbthlemi5  7283  sbthlem7  7285  caserel  7433  dmaddpi  7698  dmmulpi  7699  ltrelxr  8392  nnsscn  9318  nn0sscn  9579  nn0ssq  10044  nnssq  10045  qsscn  10047  fzval2  10431  fzossnn  10619  fzo0ssnn0  10650  infssuzcldc  10685  expcl2lemap  11009  rpexpcl  11016  expge0  11033  expge1  11034  seq3coll  11316  summodclem2a  12173  fsum3cvg3  12188  fsumrpcl  12196  fsumge0  12251  prodmodclem2a  12368  fprodrpcl  12403  fprodge0  12429  fprodge1  12431  nninfctlemfo  12842  isprm3  12921  eulerthlemrprm  13036  eulerthlema  13037  eulerthlemh  13038  eulerthlemth  13039  pcprecl  13097  pcprendvds  13098  pcpremul  13101  4sqlem11  13209  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemiex  13302  ballotfilemsima  13317  structfn  13429  strleun  13517  prdsvallem  13680  prdsval  14280  prdssca  14282  prdsbas  14283  prdsplusg  14284  prdsmulr  14285  cnfldbas  15006  mpocnfldadd  15007  mpocnfldmul  15009  cnfldcj  15011  cnfldtset  15012  cnfldle  15013  cnfldds  15014  asplss  15125  aspsubrg  15127  psrplusgg  15182  psrmulrg  15186  toponsspwpwg  15248  dmtopon  15249  lmbrf  15441  lmres  15474  txcnmpt  15499  qtopbas  15748  tgqioo  15781  dvrecap  15939  cosz12  16007  ioocosf1o  16082  efnnfsumcl  16239  efchtqdvds  16265  mpodvdsmulf1o  16284  fsumdvdsmul  16285  lgsfcl2  16330  2sqlem6  16444  2sqlem8  16447  2sqlem9  16448  trlsex  16833  eupthsg  16891