siman>

Theorem.

Arguments:

(pr), (pr),

Assertions:

(())

Proof:

Hyp	Ref	Line	Expr
	df-an	1	(()())
	pm3.27im	2	(())
1, 2	brpi21	3	(())