alexan>

Theorem.

Arguments:

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

Assertions:

(()())

Proof:

Hyp	Ref	Line	Expr
	al.imdi	1	(()())
	aln.ex	2	()
1, 2	brpi33	3	(()())
3	con	4	(()())
	df-an	5	(()())
	exn.al	6	(()())
4, 5, 6	<imtr	7	(()())
	df-an	8	(()())
8	eqt-∃-i	9	(()())
7, 9	brpi22<	10	(()())