fv-neg
Theorem.
Arguments:
(sv),
(pr),
Hypotheses:
(
)
Assertions:
(
)
Proof:
Hyp
Ref
Line
Expr
Hypo
1
(
)
1
con
2
(
)
2
im.bldal
3
(
)
ax6
4
(
)
4
con<
5
(
)
3, 5
syl
6
(
)