bitr

Theorem.

Arguments:

(pr), (pr), (pr),

Hypotheses:

()

()

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	()
		2	()
2	bi>	3	()
1	bi>	4	()
3, 4	syl	5	()
2	bi<	6	()
1	bi<	7	()
6, 7	syl	8	()
5, 8	>bii	9	()