Theorem sstri 3236

Description: Subclass transitivity inference. (Contributed by NM, 5-May-2000.)

Hypotheses

Ref	Expression
sstri.1	|- A C_ B
sstri.2	|- B C_ C

Assertion

Ref	Expression
sstri	|- A C_ C

Proof of Theorem sstri

Step	Hyp	Ref	Expression
1		sstri.1	. 2 |- A C_ B
2		sstri.2	. 2 |- B C_ C
3		sstr2 3234	. 2 |- ( A C_ B -> ( B C_ C -> A C_ C ) )
4	1, 2, 3	mp2 16	1 |- A C_ C

Syntax hints:   C_ 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  11960  fsum3cvg3  11975  fsumrpcl  11983  fsumge0  12038  prodmodclem2a  12155  fprodrpcl  12190  fprodge0  12216  fprodge1  12218  nninfctlemfo  12629  isprm3  12708  eulerthlemrprm  12819  eulerthlema  12820  eulerthlemh  12821  eulerthlemth  12822  pcprecl  12880  pcprendvds  12881  pcpremul  12884  4sqlem11  12992  structfn  13119  strleun  13205  prdsvallem  13373  prdsval  13374  prdssca  13376  prdsbas  13377  prdsplusg  13378  prdsmulr  13379  cnfldbas  14593  mpocnfldadd  14594  mpocnfldmul  14596  cnfldcj  14598  cnfldtset  14599  cnfldle  14600  cnfldds  14601  psrplusgg  14711  toponsspwpwg  14765  dmtopon  14766  lmbrf  14958  lmres  14991  txcnmpt  15016  qtopbas  15265  tgqioo  15298  dvrecap  15456  cosz12  15523  ioocosf1o  15597  mpodvdsmulf1o  15733  fsumdvdsmul  15734  lgsfcl2  15754  2sqlem6  15868  2sqlem8  15871  2sqlem9  15872  trlsex  16257  eupthsg  16315