alrot4

Theorem.

Arguments:

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

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	alcom	1	()
	alcom	2	()
2	eqt-∀-i	3	()
1, 3	bitr	4	()
4	eqt-∀-i	5	()
	alcom	6	()
	alcom	7	()
7	eqt-∀-i	8	()
5, 6, 8	2bitr	9	()