bv-idvar

Theorem.

Arguments:

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

Assertions:

( bound in ())

Proof:

Hyp	Ref	Line	Expr
	ax12	1	(()(()(()())))
	ax4	2	(()())
1, 2	rpi43	3	(()(()(()())))
	ax10	4	(()(()()))
4	aleqcom	5	(()(()()))
	ax10	6	(()(()()))
	ax10	7	(()(()()))
7	imabs	8	(()())
6, 8	rpi32	9	(()(()()))
9	aleqcom	10	(()(()()))
3, 5, 10	caseii	11	(()())
11	ax5	12	(()())
	ax7	13	(()())
12, 13	syl	14	(()())
14	df-Bvp	15	( bound in ())