dral1

Theorem.

Arguments:

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

Hypotheses:

(()())

Assertions:

(()())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(()())
1	bi>	2	(()())
2	2im.bldal	3	(()())
	bv-idvar	4	( bound in ())
3, 4	bvsyl	5	(()())
	ax10	6	(()())
5, 6	syld	7	(()())
1	bi<	8	(()())
8	2im.bldal	9	(()())
	bv-idvar	10	( bound in ())
9, 10	bvsyl	11	(()())
	ax10	12	(()())
12	aleqcom	13	(()())
11, 13	syld	14	(()())
7, 14	>bid	15	(()())