or12ass

Theorem.

Arguments:

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

Assertions:

((())(()))

Proof:

Hyp	Ref	Line	Expr
	bcom12	1	((())(()))
	df-or	2	(()())
2	bi.bldim>	3	((())(()))
	df-or	4	(()())
4	bi.bldim>	5	((())(()))
1, 3, 5	<2bitr<	6	((())(()))
	df-or	7	((())(()))
	df-or	8	((())(()))
6, 7, 8	<2bitr	9	((())(()))