Theorem sstri 2076

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

Syntax hints:   (_ wss 2050

This theorem is referenced by:  dmexg 3364  rnexg 3365  relres 3393  asymref 3445  asymref2 3446  ssrnres 3487  fabexg 3659  ssimaex 3774  oprabss 4012  sbthlem5 4457  sbthlem7 4459  rankval4 4712  rankxpl 4720  rankxplim 4722  brdom3 4811  brdom5 4812  brdom4 4813  cflim 4921  dmaddpi 5030  dmmulpi 5031  nnsscn 5930  nn0sscn 6106  uzwo5OLD 6213  flval3t 6241  nn0ssq 6263  nnssq 6264  qsscn 6266  om2uzlt2 6300  uzwo2 6458  uzinfm 6463  infmssuzle 6466  infmssuzcl 6467  seqzfn 6540  rpexpclt 6583  cau3i 6914  clm3 7079  climshft2 7106  ser1f0 7170  ivthlem4 7284  ivthlem6 7286  ivthlem7 7287  ivthlem8 7288  ivthlem9 7289  isupivth 7290  reeff1olem1 7424  lmbrf 7927  iscauf 7936  bcthlem14 8009  bcthlem15 8010  ghsubgi 8134  nvvcop 8209  nvrel 8217  nmlno0lem 8449  psdmrn 8644  pilem1 8666  pilem2 8667  efifolem1 8717  chsspwh 9114  chintcl 9290  shunssj 9334  shub1 9338  shlub 9341  shsumval2 9355  lejdi 9456  spanun 9462  sshhococ 9464  spansnpj 9496  osumcor 9582  5oa 9601  3oalem6 9607  3oa 9608  pjssm 9621  mayete3 9668  nmlnop0ALT 9915  nmcopexlem1 9946  nmcfnexlem1 9975  pjnmop 10070  pjclem1 10118  pjc 10123  mdslmd1lem1 10247  shatomistic 10283  hatomistic 10284  chpssat 10285  rnhmph 10519  relded 10644  relcat 10665

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 2054  df-ss 2056

Copyright terms: Public domain