Theorem sstri 2626

Description: Subclass transitivity inference.

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 2623	. 2 |- (A C_ B -> (B C_ C -> A C_ C))
4	1, 2, 3	mp2 54	1 |- A C_ C

Syntax hints:   C_ wss 2593

This theorem is referenced by:  uniintsn 3253  dmexg 4206  rnexg 4207  relresOLD 4243  asymrefOLD 4309  asymref2OLD 4311  ssrnres 4354  fabexg 4596  foimacnv 4657  ssimaex 4729  oprabss 4935  fparlem3 5083  fparlem4 5084  sbthlem5 5514  sbthlem7 5516  rankval4 5813  rankxpl 5821  rankxplim 5823  brdom3 5963  brdom5 5964  brdom4 5965  cflim 6057  dmaddpi 6170  dmmulpi 6171  nnsscn 7111  nn0sscn 7313  uzwo5OLD 7423  nn0ssq 7442  nnssq 7443  qsscn 7445  flval3 7479  uzwo2 7626  uzinfmi 7631  infmssuzle 7634  infmssuzleOLD 7635  infmssuzcl 7636  om2uzlt2i 7710  seqzfn 7782  rpexpcl 7825  cau3ii 8166  clm3i 8339  climshft2i 8366  ivthlem4 8546  ivthlem6 8548  ivthlem7 8549  ivthlem8 8550  ivthlem9 8551  isupivthi 8552  reeff1olem1 8689  lmbrf 9208  iscauf 9217  bcthlem14 9290  bcthlem15 9291  ghsubgi 9446  nvvcop 9545  nvrel 9553  nmlno0lem 9793  psdmrn 9991  pilem1 10020  pilem2 10021  efifolem1 10076  hausfillim 10303  dirdm 10354  on1el3 10412  chsspwh 10752  chintcli 10928  shunssji 10972  shub1i 10976  shlubi 10979  shsumval2i 10993  lejdii 11094  spanuni 11100  sshhococi 11102  spansnpji 11134  osumcori 11222  5oai 11241  3oalem6 11247  3oai 11248  pjssmii 11261  mayete3i 11308  mayete3OLDi 11309  mayetes3i 11310  nmlnop0iALT 11557  nmcopexlem1 11588  nmcfnexlem1 11617  pjnmopi 11719  pjclem1 11768  pjci 11773  mdslmd1lem1 11897  shatomistici 11933  hatomistici 11934  chpssati 11935  bnj1145 13431  bnj1286 13481  divalglem8 13703  gcdcllem3 13720  isprm3 13776  txpss3v 14065  txprel 14066  dffprod 14670  rnhmph 14887  relded 15087  relcat 15108  finminlem 15367  flimcls 15588  tailf 15633  istail 15634  tailmap 15636  filnetlem1 15640  fsumltisumii 15822  metdcn 15853  iiuni 15868  dfii3 15870  tlmval 15903  totbndbnd 15944  heiborlem6 15960  heiborlem11 15965  heiborlem12 15966  heiborlem14 15968  heiborlem15 15969  heiborlem16 15970  heiborlem17 15971  rrntotbnd 16022  reheibor 16025  phtpycom 16050  phtpycolem3 16053  phtpycolem4 16054  reparphtlem2 16064  pcocn 16076  pcohtpylem3 16082  pcopt 16084  pcoass 16085  pcorevlem 16086  pcorev 16087  pi1gp 16095  stbcl 16730  hlatmstc 17047  hlatle 17048  pmaple 17241  sspadd1 17276  sspadd2 17277

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-in 2603  df-ss 2605

Copyright terms: Public domain