im.bidi

Theorem.

Arguments:

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

Assertions:

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

Proof:

Hyp	Ref	Line	Expr
	bi>	1	(()())
1	syl<	2	((())(()))
2	ax2	3	((())(()()))
	bi<	4	(()())
4	syl<	5	((())(()))
5	ax2	6	((())(()()))
3, 6	>bid	7	((())(()()))
	bi>	8	((()())(()()))
8	ax2-converse	9	((()())(()))
	bi<	10	((()())(()()))
10	ax2-converse	11	((()())(()))
9, 11	im.bldan<>d	12	((()())(()(()())))
	anidm	13	(())
13	bicomi	14	(())
	dfbi	15	(()(()()))
12, 14, 15	<imtrg	16	((()())(()))
7, 16	>bii	17	((())(()()))