Theorem sstri 1512

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

Syntax hints:   (_ wss 1487

This theorem is referenced by:  relres 2591  sbthlem5 3353  sbthlem7 3355  ranklon 3540  cflim 3704  dmaddpi 3812  dmmulpi 3813  nnsscn 4426  nn0sscn 4539  uzwo2 4606  nn0ssq 4634  nnssq 4635  qsscn 4637  chintcl 5296  shunssj 5340  shub1 5344  shlub 5347  shsumval2 5361  spanun 5450  sshhococ 5451  spansnpj 5481  cmle 5511  5oa 5551  3oalem6 5557  3oa 5558  pjssm 5572  pjclem1 5649  pjc 5654  hatomistic 5755  chpssat 5756

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-in 1491  df-ss 1492

metamath.org