cbval-dv

Theorem.

Arguments:

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

Distinct variable conditions:

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

Hypotheses:

(()())

( bound in )

( bound in )

Assertions:

()

Proof:

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