Theorem sstri 2073

Description: Subclass transitivity inference.

Hypotheses

Ref	Expression
sstri.1	|- A (_ B
sstri.2	|- B (_ C

Assertion

Ref	Expression
sstri	|- A (_ C

Proof of Theorem sstri

Step	Hyp	Ref	Expression
1		sstri.1	. 2 |- A (_ B
2		sstri.2	. 2 |- B (_ C
3		sstr2 2071	. 2 |- (A (_ B -> (B (_ C -> A (_ C))
4	1, 2, 3	mp2 43	1 |- A (_ C

Syntax hints:   (_ wss 2047

This theorem is referenced by:  dmexg 3358  rnexg 3359  relres 3387  asymref 3439  asymref2 3440  ssrnres 3481  fabexg 3653  ssimaex 3768  oprabss 4006  sbthlem5 4451  sbthlem7 4453  rankval4 4702  rankxpl 4710  rankxplim 4712  brdom3 4801  brdom5 4802  brdom4 4803  cflim 4909  dmaddpi 5018  dmmulpi 5019  nnsscn 5928  nn0sscn 6104  uzwo5OLD 6211  flval3t 6239  nn0ssq 6262  nnssq 6263  qsscn 6265  om2uzlt2 6299  uzwo2 6457  uzinfm 6462  infmssuzle 6465  infmssuzcl 6466  seqzfn 6539  rpexpclt 6582  cau3i 6914  clm3 7079  climshft2 7106  ser1f0 7170  ivthlem4 7284  ivthlem6 7286  ivthlem7 7287  ivthlem8 7288  ivthlem9 7289  isupivth 7290  reeff1olem1 7424  lmbrf 7930  iscauf 7939  bcthlem14 8012  bcthlem15 8013  ghsubgi 8138  nvvcop 8213  nvrel 8221  nmlno0lem 8453  psdmrn 8648  pilem1 8671  pilem2 8672  efifolem1 8722  chsspwh 9119  chintcl 9295  shunssj 9339  shub1 9343  shlub 9346  shsumval2 9360  lejdi 9461  spanun 9467  sshhococ 9469  spansnpj 9501  osumcor 9587  5oa 9606  3oalem6 9612  3oa 9613  pjssm 9626  mayete3 9673  nmlnop0ALT 9920  nmcopexlem1 9951  nmcfnexlem1 9980  pjnmop 10075  pjclem1 10123  pjc 10128  mdslmd1lem1 10252  shatomistic 10288  hatomistic 10289  chpssat 10290  rnhmph 10533  relded 10673  relcat 10694

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053

Copyright terms: Public domain