Theorem sstri 2071

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 2069	. 2 |- (A (_ B -> (B (_ C -> A (_ C))
4	1, 2, 3	mp2 43	1 |- A (_ C

Syntax hints:   (_ wss 2045

This theorem is referenced by:  dmexg 3355  rnexg 3356  relres 3384  asymref 3436  asymref2 3437  ssrnres 3478  fabexg 3650  ssimaex 3765  oprabss 4003  sbthlem5 4444  sbthlem7 4446  rankval4 4689  rankxpl 4697  rankxplim 4699  brdom3 4788  brdom5 4789  brdom4 4790  cflim 4896  dmaddpi 5005  dmmulpi 5006  nnsscn 5890  nn0sscn 6065  uzwo5OLD 6173  flval3t 6200  nn0ssq 6217  nnssq 6218  qsscn 6220  om2uzlt2 6254  uzwo2 6407  uzinfm 6412  infmssuzle 6415  infmssuzcl 6416  seqzfn 6489  rpexpclt 6532  cau3i 6880  clm3 7047  climshft2 7074  ser1f0 7141  ivthlem4 7255  ivthlem6 7257  ivthlem7 7258  ivthlem8 7259  ivthlem9 7260  isupivth 7261  ivthlem4OLD 7264  ivthOLD 7269  ivth2OLD 7270  reeff1olem1 7400  reeff1olem1OLD 7402  lmbrf 7913  iscauf 7922  bcthlem14 7995  bcthlem15 7996  ghsubgi 8123  nvvcop 8198  nvrel 8206  nmlno0lem 8438  psdmrn 8631  pilem1 8654  pilem2 8655  efifolem1 8701  chsspwh 9107  chintcl 9283  shunssj 9327  shub1 9331  shlub 9334  shsumval2 9348  lejdi 9449  spanun 9455  sshhococ 9457  spansnpj 9491  osumcor 9577  5oa 9597  3oalem6 9603  3oa 9604  pjssm 9617  mayete3 9664  nmlnop0ALT 9911  nmcopexlem1 9942  nmcfnexlem1 9971  pjnmop 10066  pjclem1 10114  pjc 10119  mdslmd1lem1 10243  shatomistic 10279  hatomistic 10280  chpssat 10281  rnhmph 10514  relded 10624  relcat 10645

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459

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

Copyright terms: Public domain