mo-sb1

Theorem.

Arguments:

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

Dummy variables:

(sv),

Distinct variable conditions:

(, ), (, ), (, ), (, ),

Assertions:

((()))

Proof:

Hyp	Ref	Line	Expr
	eqt>	1	(()(()()))
1	bi.bldim>d	2	(()((())(())))
2	bi.bldald	3	(()((())(())))
	ax17-bv	4	( bound in (()))
3, 4	sb-xplw	5	((())[/](()))
5	sb-spec-ex	6	((())(()))
	df-∃mo-alt2	7	((()))
6, 7	syl	8	((()))