cbv2-dv

Theorem.

Arguments:

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

Distinct variable conditions:

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

Hypotheses:

((()()))

(())

(())

Assertions:

(())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	((()()))
		2	(())
		3	(())
	bi>	4	(()())
1, 4	rpi33	5	((()()))
2, 3, 5	cbv1-dv	6	(())
	bi<	7	(()())
1, 7	rpi33	8	((()()))
	eqcomi	9	(()())
8, 9	rpi32	10	((()()))
2, 3, 10	cbv1-dv	11	(())
	ax7	12	()
11, 12	syl	13	(())
6, 13	>bid	14	(())