chvar-∀-1w

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Assertions:

([/][/])

Proof:

Hyp	Ref	Line	Expr
	dfsb-dval	1	([/](()))
1	eqt-∀-i	2	([/](()))
	alcom	3	((())(()))
	com	4	(()())
4	bi.bldim<	5	((())(()))
5	eqt-∀-i	6	((())(()))
	dfsb-dval	7	([/](()))
6, 7	><bitr	8	((())[/])
8	eqt-∀-i	9	((())[/])
2, 3, 9	2bitr	10	([/][/])