fv-imd

Theorem.

Arguments:

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

Hypotheses:

(())

(())

( bound in )

Assertions:

((()()))

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(())
		2	(())
		3	( bound in )
2, 3	fv-negd	4	(())
4	com12i	5	(())
	<neg	6	(())
6	im.bldal	7	(())
5, 7	rpi33	8	((()))
1	com12i	9	(())
	ax1	10	(())
10	im.bldal	11	(())
9, 11	rpi33	12	((()))
8, 12	ja-pre	13	(()(()))
13	com12i	14	((()()))