impexp

Theorem.

Arguments:

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

Assertions:

((())(()))

Proof:

Hyp	Ref	Line	Expr
	df-an	1	(()())
1	bi.bldim<	2	((())(()))
	imp-pre	3	((())(()))
	exp-pre	4	((())(()))
3, 4	>bii	5	((())(()))
2, 5	bitr	6	((())(()))