cbv1-dv

Theorem.

Arguments:

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

Distinct variable conditions:

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

Hypotheses:

((()()))

(())

(())

Assertions:

(())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	((()()))
		2	(())
		3	(())
	ax4	4	()
3, 4	syl	5	(())
5	2im.bldal	6	(())
	ax7	7	()
6, 7	rpi33	8	(())
1	com23i	9	(((())))
2, 9	rpi33d	10	(((())))
10	2im.bldal	11	(((())))
	ax9alt	12	((()))
11, 12	rpi33	13	(())
13	2im.bldal	14	(())
	ax7	15	()
14, 15	syl	16	(())
8, 16	syld	17	(())