case

Theorem.

Arguments:

(pr), (pr),

Assertions:

(()(()))

Proof:

Hyp	Ref	Line	Expr
	syl<	1	(()(()()))
	neg+	2	(())
1, 2	rpi33	3	(()(()))
	con<	4	(()())
3, 4	rpi32	5	(()(()))