bitrd
Theorem.
Arguments:
(pr),
(pr),
(pr),
(pr),
Hypotheses:
(
(
))
(
(
))
Assertions:
(
(
))
Proof:
Hyp
Ref
Line
Expr
Hypo
1
(
(
))
2
(
(
))
2
bi>
3
(
(
))
1
bi>
4
(
(
))
3, 4
syld
5
(
(
))
1
bi<
6
(
(
))
2
bi<
7
(
(
))
6, 7
syld
8
(
(
))
5, 8
>bid
9
(
(
))