Theorem sstri 2077

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

Syntax hints:   (_ wss 2051

This theorem is referenced by:  dmexg 3365  rnexg 3366  relres 3394  asymref 3446  asymref2 3447  ssrnres 3488  fabexg 3660  ssimaex 3775  oprabss 4013  sbthlem5 4458  sbthlem7 4460  rankval4 4719  rankxpl 4727  rankxplim 4729  brdom3 4818  brdom5 4819  brdom4 4820  cflim 4928  dmaddpi 5037  dmmulpi 5038  nnsscn 5937  nn0sscn 6113  uzwo5OLD 6220  flval3t 6248  nn0ssq 6270  nnssq 6271  qsscn 6273  om2uzlt2 6307  uzwo2 6465  uzinfm 6470  infmssuzle 6473  infmssuzcl 6474  seqzfn 6547  rpexpclt 6590  cau3i 6921  clm3 7086  climshft2 7113  ser1f0 7177  ivthlem4 7291  ivthlem6 7293  ivthlem7 7294  ivthlem8 7295  ivthlem9 7296  isupivth 7297  reeff1olem1 7431  lmbrf 7934  iscauf 7943  bcthlem14 8016  bcthlem15 8017  ghsubgi 8141  nvvcop 8216  nvrel 8224  nmlno0lem 8456  psdmrn 8651  pilem1 8673  pilem2 8674  efifolem1 8724  chsspwh 9121  chintcl 9297  shunssj 9341  shub1 9345  shlub 9348  shsumval2 9362  lejdi 9463  spanun 9469  sshhococ 9471  spansnpj 9503  osumcor 9589  5oa 9608  3oalem6 9614  3oa 9615  pjssm 9628  mayete3 9675  nmlnop0ALT 9922  nmcopexlem1 9953  nmcfnexlem1 9982  pjnmop 10077  pjclem1 10126  pjc 10131  mdslmd1lem1 10255  shatomistic 10291  hatomistic 10292  chpssat 10293  rnhmph 10527  relded 10652  relcat 10673

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2055  df-ss 2057

Copyright terms: Public domain