bi.bldan>d

Theorem.

Arguments:

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

Hypotheses:

(())

Assertions:

((()()))

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(())
1	bi>	2	(())
2	im.bldan>d	3	((()()))
1	bi<	4	(())
4	im.bldan>d	5	((()()))
3, 5	>bid	6	((()()))