ex.andi
Theorem.
Arguments:
(sv),
(pr),
(pr),
Assertions:
(
(
)
(
))
Proof:
Hyp
Ref
Line
Expr
siman<
1
((
)
)
1
im.bldex
2
(
(
)
)
siman>
3
((
)
)
3
im.bldex
4
(
(
)
)
2, 4
jca
5
(
(
)
(
))