an.ordi<

Theorem.

Arguments:

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

Assertions:

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

Proof:

Hyp	Ref	Line	Expr
	or.andi<	1	((())(()()))
	nor.an	2	(()())
2	bi.bldor>	3	((())(()))
	nan.or	4	(()())
	nan.or	5	(()())
4, 5	bi.bldan<>	6	((()())(()()))
1, 3, 6	<2bitr	7	((())(()()))
7	bi.bldneg	8	((())(()()))
	an.or	9	((())(()))
	or.an	10	((()())(()()))
8, 9, 10	<2bitr	11	((())(()()))