imgen>

Theorem.

Arguments:

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

Hypotheses:

( bound in )

Assertions:

(()())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
1	df-Bvp	2	()
	al.imdi	3	(()())
2, 3	rpi32	4	(()())
	fv-alx	5	()
2, 5	fv-im	6	(()())
	ax4	7	()
7	syl<	8	(()())
8	im.bldal	9	(()())
6, 9	syl	10	(()())
4, 10	>bii	11	(()())