drex1

Theorem.

Arguments:

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

Hypotheses:

(()())

Assertions:

(()())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(()())
1	bi.bldnegd	2	(()())
2	dral1	3	(()())
3	bi.bldnegd	4	(()())
	df-ex	5	()
	df-ex	6	()
4, 5, 6	<2bitrg	7	(()())