spec

Theorem.

Arguments:

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

Dummy variables:

(sv),

Distinct variable conditions:

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

Assertions:

([/])

Proof:

Hyp	Ref	Line	Expr
	spec-w	1	([/])
1	imgen>i	2	([/])
	spec-w	3	([/][/][/])
	sbco2w	4	([/][/][/])
2, 3, 4	3syl	5	([/])