chvar-∀-w

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Hypotheses:

( bound in )

Assertions:

([/])

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
	chvar-∀-1w	2	([/][/])
1	sb-bv	3	([/])
3	eqt-∀-i	4	([/])
2, 4	bitr	5	([/])