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  3818  snsstp2  3819  elopabran  4372  nnregexmid  4713  dmexg  4988  rnexg  4989  ssrnres  5171  cossxp  5251  cocnvss  5254  funinsn  5370  fabexg  5515  foimacnv  5592  ssimaex  5697  oprabss  6096  tposssxp  6401  mapsspw  6839  sbthlemi5  7139  sbthlem7  7141  caserel  7265  dmaddpi  7523  dmmulpi  7524  ltrelxr  8218  nnsscn  9126  nn0sscn  9385  nn0ssq  9835  nnssq  9836  qsscn  9838  fzval2  10219  fzossnn  10402  fzo0ssnn0  10433  infssuzcldc  10467  expcl2lemap  10785  rpexpcl  10792  expge0  10809  expge1  10810  seq3coll  11077  summodclem2a  11907  fsum3cvg3  11922  fsumrpcl  11930  fsumge0  11985  prodmodclem2a  12102  fprodrpcl  12137  fprodge0  12163  fprodge1  12165  nninfctlemfo  12576  isprm3  12655  eulerthlemrprm  12766  eulerthlema  12767  eulerthlemh  12768  eulerthlemth  12769  pcprecl  12827  pcprendvds  12828  pcpremul  12831  4sqlem11  12939  structfn  13066  strleun  13152  prdsvallem  13320  prdsval  13321  prdssca  13323  prdsbas  13324  prdsplusg  13325  prdsmulr  13326  cnfldbas  14539  mpocnfldadd  14540  mpocnfldmul  14542  cnfldcj  14544  cnfldtset  14545  cnfldle  14546  cnfldds  14547  psrplusgg  14657  toponsspwpwg  14711  dmtopon  14712  lmbrf  14904  lmres  14937  txcnmpt  14962  qtopbas  15211  tgqioo  15244  dvrecap  15402  cosz12  15469  ioocosf1o  15543  mpodvdsmulf1o  15679  fsumdvdsmul  15680  lgsfcl2  15700  2sqlem6  15814  2sqlem8  15817  2sqlem9  15818