sbco2

Theorem.

Arguments:

(st), (sv), (sv), (pr),

Dummy variables:

(sv),

Distinct variable conditions:

(, ), (, ), (, ), (, ),

Hypotheses:

( bound in )

Assertions:

([/][/][/])

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
	ax17-bv	2	( bound in [/])
	ax17-bv	3	( bound in )
1	bv-sb-d1	4	( bound in [/])
2	sbco2w	5	([/][/][/][/][/])
4	sbco2w	6	([/][/][/][/][/])
	sbid	7	([/][/][/])
6, 7	bitr	8	([/][/][/][/])
3	sbco2w	9	([/][/][/])
9	bi.bldsb	10	([/][/][/][/][/])
8, 10	<>bitr	11	([/][/][/])
11	bi.bldsb	12	([/][/][/][/][/])
3	sbco2w	13	([/][/][/])
12, 13	bitr	14	([/][/][/][/])
5, 14	<>bitr	15	([/][/][/])