fv-bid

Theorem.

Arguments:

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

Hypotheses:

(())

(())

( bound in )

Assertions:

((()()))

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(())
		2	(())
		3	( bound in )
1, 2, 3	fv-imd	4	((()()))
1, 2, 3	fv-imd	5	((()()))
4, 5	im.bldan<>d	6	(((()())(()())))
	dfbi	7	(()(()()))
	al.dfbi	8	(()(()()))
6, 7, 8	<imtrg	9	((()()))