dveeq1

Theorem.

Arguments:

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

Dummy variables:

(sv),

Distinct variable conditions:

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

Assertions:

(()(()()))

Proof:

Hyp	Ref	Line	Expr
	ax12	1	(()(()(()())))
1	com12i	2	(()(()(()())))
	ax16	3	(()(()()))
3	ax1	4	(()(()(()())))
2, 4	casei	5	(()(()()))