ax4c1

Theorem.

Arguments:

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

Hypotheses:

(()())

(())

( bound in )

Assertions:

(())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(()())
		2	(())
		3	( bound in )
3	df-Bvp	4	()
4	adan>	5	(())
2	imp	6	(())
5, 6	jca	7	(()())
	al.andi	8	(()())
7, 8	brpi22<	9	(()())
1	adan<	10	(()(()))
9	df-Bvp	11	( bound in ())
10, 11	ax4c	12	(())
12	exp	13	(())