eqvini

Theorem.

Arguments:

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

Distinct variable conditions:

(, ), (, ),

Assertions:

(()(()()))

Proof:

Hyp	Ref	Line	Expr
	eqtr	1	(()(()()))
1	eqcomi	2	(()(()()))
2	com12i	3	(()(()()))
3	imp	4	((()())())
	idd	5	(()(()()))
5	imp	6	((()())())
4, 6	jca	7	((()())(()()))
7	exp	8	(()(()(()())))
	ax17-bv	9	( bound in ())
8	im.bldexd	10	(()(()(()())))
	ax9ex	11	()
	eqcomi	12	(()())
12	im.bldex	13	(()())
11, 13	ax-mp	14	()
10, 14	mpi	15	(()(()()))