cbv3

Theorem.

Arguments:

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

Hypotheses:

(()())

( bound in )

( bound in )

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(()())
		2	( bound in )
		3	( bound in )
3	df-Bvp	4	()
4	syl<	5	(()())
2	df-Bvp	6	()
6	ax1	7	(()())
1	ax1	8	(()(()()))
5, 7, 8	cbv1	9	(()())
	id	10	()
10	ax-gen	11	()
11	ax-gen	12	()
9, 12	ax-mp	13	()