cbv1

Theorem.

Arguments:

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

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-sv	12	((()))
11, 12	rpi33	13	(())
13	2im.bldal	14	(())
	ax7	15	()
14, 15	syl	16	(())
8, 16	syld	17	(())