dfbi

Theorem.

Arguments:

(pr), (pr),

Assertions:

(()(()()))

Proof:

Hyp	Ref	Line	Expr
	dfbi2	1	(()(()()))
	df-an	2	((()())(()()))
1, 2	><bitr	3	(()(()()))