ax9alt

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Assertions:

((()))

Proof:

Hyp	Ref	Line	Expr
	ax9	1	()
	df-ex	2	(()())
1, 2	bmp<	3	()
	im.bldext	4	((())(()))
3, 4	mpi	5	((()))
	ax6e	6	()
5, 6	syl	7	((()))