sb-spec-ex
Theorem.
Arguments:
(st),
(sv),
(pr),
Assertions:
([
/
]
)
Proof:
Hyp
Ref
Line
Expr
spec
1
(
[
/
]
)
sb-neg
2
([
/
]
[
/
]
)
1, 2
brpi22
3
(
[
/
]
)
3
con>
4
([
/
]
)
df-ex
5
(
)
4, 5
brpi22<
6
([
/
]
)
(st), 
(sv), 
(pr), (st), (sv), (pr), /]
)
[/])/]
[/])[/])/]))/])