Theorem sstri 3233

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

Syntax hints:   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  difdif2ss  3461  difdifdirss  3576  snsstp1  3817  snsstp2  3818  elopabran  4371  nnregexmid  4712  dmexg  4987  rnexg  4988  ssrnres  5170  cossxp  5250  cocnvss  5253  funinsn  5369  fabexg  5512  foimacnv  5589  ssimaex  5694  oprabss  6089  tposssxp  6393  mapsspw  6829  sbthlemi5  7124  sbthlem7  7126  caserel  7250  dmaddpi  7508  dmmulpi  7509  ltrelxr  8203  nnsscn  9111  nn0sscn  9370  nn0ssq  9819  nnssq  9820  qsscn  9822  fzval2  10203  fzossnn  10385  fzo0ssnn0  10416  infssuzcldc  10450  expcl2lemap  10768  rpexpcl  10775  expge0  10792  expge1  10793  seq3coll  11059  summodclem2a  11887  fsum3cvg3  11902  fsumrpcl  11910  fsumge0  11965  prodmodclem2a  12082  fprodrpcl  12117  fprodge0  12143  fprodge1  12145  nninfctlemfo  12556  isprm3  12635  eulerthlemrprm  12746  eulerthlema  12747  eulerthlemh  12748  eulerthlemth  12749  pcprecl  12807  pcprendvds  12808  pcpremul  12811  4sqlem11  12919  structfn  13046  strleun  13132  prdsvallem  13300  prdsval  13301  prdssca  13303  prdsbas  13304  prdsplusg  13305  prdsmulr  13306  cnfldbas  14518  mpocnfldadd  14519  mpocnfldmul  14521  cnfldcj  14523  cnfldtset  14524  cnfldle  14525  cnfldds  14526  psrplusgg  14636  toponsspwpwg  14690  dmtopon  14691  lmbrf  14883  lmres  14916  txcnmpt  14941  qtopbas  15190  tgqioo  15223  dvrecap  15381  cosz12  15448  ioocosf1o  15522  mpodvdsmulf1o  15658  fsumdvdsmul  15659  lgsfcl2  15679  2sqlem6  15793  2sqlem8  15796  2sqlem9  15797