Theorem sstri 3247

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

Syntax hints:   ⊆ wss 3211

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  difdif2ss  3478  difdifdirss  3594  snsstp1  3844  snsstp2  3845  elopabran  4402  nnregexmid  4743  dmexg  5021  rnexg  5022  ssrnres  5205  cossxp  5285  cocnvss  5288  funinsn  5405  fabexg  5554  foimacnv  5632  ssimaex  5738  oprabss  6139  tposssxp  6480  mapsspw  6918  sbthlemi5  7231  sbthlem7  7233  caserel  7378  dmaddpi  7640  dmmulpi  7641  ltrelxr  8334  nnsscn  9242  nn0sscn  9501  nn0ssq  9960  nnssq  9961  qsscn  9963  fzval2  10345  fzossnn  10529  fzo0ssnn0  10560  infssuzcldc  10595  expcl2lemap  10913  rpexpcl  10920  expge0  10937  expge1  10938  seq3coll  11214  summodclem2a  12067  fsum3cvg3  12082  fsumrpcl  12090  fsumge0  12145  prodmodclem2a  12262  fprodrpcl  12297  fprodge0  12323  fprodge1  12325  nninfctlemfo  12736  isprm3  12815  eulerthlemrprm  12926  eulerthlema  12927  eulerthlemh  12928  eulerthlemth  12929  pcprecl  12987  pcprendvds  12988  pcpremul  12991  4sqlem11  13099  structfn  13231  strleun  13317  prdsvallem  13485  prdsval  13486  prdssca  13488  prdsbas  13489  prdsplusg  13490  prdsmulr  13491  cnfldbas  14708  mpocnfldadd  14709  mpocnfldmul  14711  cnfldcj  14713  cnfldtset  14714  cnfldle  14715  cnfldds  14716  psrplusgg  14833  toponsspwpwg  14887  dmtopon  14888  lmbrf  15080  lmres  15113  txcnmpt  15138  qtopbas  15387  tgqioo  15420  dvrecap  15578  cosz12  15645  ioocosf1o  15719  mpodvdsmulf1o  15858  fsumdvdsmul  15859  lgsfcl2  15879  2sqlem6  15993  2sqlem8  15996  2sqlem9  15997  trlsex  16382  eupthsg  16440