or.andi<

Theorem.

Arguments:

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

Assertions:

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

Proof:

Hyp	Ref	Line	Expr
	siman<	1	(())
1	im.bldor>	2	((())())
	siman>	3	(())
3	im.bldor>	4	((())())
2, 4	jca	5	((())(()()))
	>andc	6	(()(()(())))
	df-or	7	(()())
	df-or	8	((())(()))
6, 7, 8	<imtrg	9	(()(()(())))
	df-or	10	(()())
9, 10	brpi21	11	(()(()(())))
11	imp	12	((()())(()))
5, 12	>bii	13	((())(()()))