ax9alt-sv

Theorem.

Arguments:

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

Assertions:

((()))

Proof:

Hyp	Ref	Line	Expr
	ax9-sv	1	()
	im.bldext	2	((())(()))
1, 2	mpi	3	((()))
	ax6e	4	()
3, 4	syl	5	((()))