an.or2di

Theorem.

Arguments:

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

Assertions:

((()())((()())(()())))

Proof:

Hyp	Ref	Line	Expr
	an.ordi>	1	((()())((())(())))
	an.ordi<	2	((())(()()))
	an.ordi<	3	((())(()()))
2, 3	bi.bldor<>	4	(((())(()))((()())(()())))
1, 4	bitr	5	((()())((()())(()())))