pm3.27im

Theorem.

Arguments:

(pr), (pr),

Assertions:

(())

Proof:

Hyp	Ref	Line	Expr
	ax1	1	(())
1	con<	2	(())