cbvexd

Theorem.

Arguments:

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

Distinct variable conditions:

(, ), (, ),

Hypotheses:

((()()))

(())

( bound in )

Assertions:

(())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	((()()))
		2	(())
		3	( bound in )
2, 3	fv-negd	4	(())
	conb	5	(()())
1, 5	brpi33	6	((()()))
3, 4, 6	cbvald	7	(())
7	bi.bldnegd	8	(())
	df-ex	9	()
	df-ex	10	()
8, 9, 10	<2bitrg	11	(())