exan>

Theorem.

Arguments:

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

Hypotheses:

( bound in )

Assertions:

(()())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
	df-ex	2	(()())
1	bv-¬	3	( bound in )
3	alor>	4	(()())
	nan.or	5	(()())
5	eqt-∀-i	6	(()())
	nan.or	7	(()())
	aln.ex	8	()
8	bi.bldor<	9	(()())
7, 9	><bitr	10	(()())
4, 6, 10	<2bitr	11	(()())
11	conb>i	12	(()())
2, 12	><bitr	13	(()())