al-ex
Theorem.
Arguments:
(sv),
(pr),
Assertions:
(
)
Proof:
Hyp
Ref
Line
Expr
ax4
1
(
)
spec-ex
2
(
)
1, 2
syl
3
(
)