eu-sb1

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Assertions:

(([/](())))

Proof:

Hyp	Ref	Line	Expr
	siman>	1	(([/](()))(()))
1	mo-sb1	2	(([/](())))
	siman<	3	(([/](()))[/])
3	sb-spec-ex	4	(([/](())))
2, 4	jca	5	(([/](()))())
	df-∃1-alt5	6	(())
5, 6	brpi22<	7	(([/](())))