ax9-sv

Theorem.

Arguments:

(sv), (sv),

Dummy variables:

(sv),

Distinct variable conditions:

(, ), (, ),

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	ax9ex	1	()
	al-ex	2	(()())
	ax12	3	(()(()(()())))
	ax16	4	(()(()()))
4	ax1	5	(()(()(()())))
3, 5	casei	6	(()(()()))
	bv-∀b	7	( bound in ())
7	bv-¬	8	( bound in ())
	eqt<	9	(()(()()))
9	ax1	10	(()(()(()())))
6, 8, 10	cbvexd-dv	11	(()(()()))
1, 11	bmpi>	12	(()())
2, 12	casei	13	()

Theorems: