Theorem sstri 3237

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

Syntax hints:   ⊆ wss 3201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  difdif2ss  3466  difdifdirss  3581  snsstp1  3828  snsstp2  3829  elopabran  4384  nnregexmid  4725  dmexg  5002  rnexg  5003  ssrnres  5186  cossxp  5266  cocnvss  5269  funinsn  5386  fabexg  5532  foimacnv  5610  ssimaex  5716  oprabss  6117  tposssxp  6458  mapsspw  6896  sbthlemi5  7203  sbthlem7  7205  caserel  7329  dmaddpi  7588  dmmulpi  7589  ltrelxr  8282  nnsscn  9190  nn0sscn  9449  nn0ssq  9906  nnssq  9907  qsscn  9909  fzval2  10291  fzossnn  10475  fzo0ssnn0  10506  infssuzcldc  10541  expcl2lemap  10859  rpexpcl  10866  expge0  10883  expge1  10884  seq3coll  11152  summodclem2a  12005  fsum3cvg3  12020  fsumrpcl  12028  fsumge0  12083  prodmodclem2a  12200  fprodrpcl  12235  fprodge0  12261  fprodge1  12263  nninfctlemfo  12674  isprm3  12753  eulerthlemrprm  12864  eulerthlema  12865  eulerthlemh  12866  eulerthlemth  12867  pcprecl  12925  pcprendvds  12926  pcpremul  12929  4sqlem11  13037  structfn  13164  strleun  13250  prdsvallem  13418  prdsval  13419  prdssca  13421  prdsbas  13422  prdsplusg  13423  prdsmulr  13424  cnfldbas  14639  mpocnfldadd  14640  mpocnfldmul  14642  cnfldcj  14644  cnfldtset  14645  cnfldle  14646  cnfldds  14647  psrplusgg  14762  toponsspwpwg  14816  dmtopon  14817  lmbrf  15009  lmres  15042  txcnmpt  15067  qtopbas  15316  tgqioo  15349  dvrecap  15507  cosz12  15574  ioocosf1o  15648  mpodvdsmulf1o  15787  fsumdvdsmul  15788  lgsfcl2  15808  2sqlem6  15922  2sqlem8  15925  2sqlem9  15926  trlsex  16311  eupthsg  16369