ax17eq

Theorem.

Arguments:

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

Distinct variable conditions:

(, ), (, ),

Assertions:

( bound in ())

Proof:

Hyp	Ref	Line	Expr
	ax12	1	(()(()(()())))
	ax16	2	(()(()()))
	ax16	3	(()(()()))
1, 2, 3	caseii	4	(()())
4	df-Bvp	5	( bound in ())