eqs4lem

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Assertions:

((())(()))

Proof:

Hyp	Ref	Line	Expr
	ax4	1	((())(()))
	ax4	2	((())(()))
1, 2	msca	3	((())(()(())))
	fv-nalx	4	( bound in (()))
4	df-Bvp	5	((())(()))
3, 5	rpi33	6	((())(()(())))
6	ax5	7	((())(()(())))
	ax9alt	8	((()(()))(()))
7, 8	syl	9	((())(()))
	eqs3lem	10	((())(()))
9, 10	brpi22<	11	((())(()))

Theorems: