Theorem sstri 3236

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

Syntax hints:   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  difdif2ss  3464  difdifdirss  3579  snsstp1  3823  snsstp2  3824  elopabran  4378  nnregexmid  4719  dmexg  4996  rnexg  4997  ssrnres  5179  cossxp  5259  cocnvss  5262  funinsn  5379  fabexg  5524  foimacnv  5601  ssimaex  5707  oprabss  6107  tposssxp  6415  mapsspw  6853  sbthlemi5  7160  sbthlem7  7162  caserel  7286  dmaddpi  7545  dmmulpi  7546  ltrelxr  8240  nnsscn  9148  nn0sscn  9407  nn0ssq  9862  nnssq  9863  qsscn  9865  fzval2  10246  fzossnn  10430  fzo0ssnn0  10461  infssuzcldc  10496  expcl2lemap  10814  rpexpcl  10821  expge0  10838  expge1  10839  seq3coll  11107  summodclem2a  11947  fsum3cvg3  11962  fsumrpcl  11970  fsumge0  12025  prodmodclem2a  12142  fprodrpcl  12177  fprodge0  12203  fprodge1  12205  nninfctlemfo  12616  isprm3  12695  eulerthlemrprm  12806  eulerthlema  12807  eulerthlemh  12808  eulerthlemth  12809  pcprecl  12867  pcprendvds  12868  pcpremul  12871  4sqlem11  12979  structfn  13106  strleun  13192  prdsvallem  13360  prdsval  13361  prdssca  13363  prdsbas  13364  prdsplusg  13365  prdsmulr  13366  cnfldbas  14580  mpocnfldadd  14581  mpocnfldmul  14583  cnfldcj  14585  cnfldtset  14586  cnfldle  14587  cnfldds  14588  psrplusgg  14698  toponsspwpwg  14752  dmtopon  14753  lmbrf  14945  lmres  14978  txcnmpt  15003  qtopbas  15252  tgqioo  15285  dvrecap  15443  cosz12  15510  ioocosf1o  15584  mpodvdsmulf1o  15720  fsumdvdsmul  15721  lgsfcl2  15741  2sqlem6  15855  2sqlem8  15858  2sqlem9  15859  trlsex  16244  eupthsg  16302