bmpg>
Theorem.
Arguments:
(sv),
(pr),
(pr),
Hypotheses:
(
)
Assertions:
Proof:
Hyp
Ref
Line
Expr
Hypo
1
2
(
)
2
bi>
3
(
)
1, 3
mpg
4