chvar-∀

Theorem.

Arguments:

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

Dummy variables:

(sv),

Distinct variable conditions:

(, ), (, ), (, ),

Hypotheses:

( bound in )

Assertions:

([/])

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
	ax17-bv	2	( bound in )
1	bv-sb-d1	3	( bound in [/])
2	chvar-∀-w	4	([/])
3	chvar-∀-w	5	([/][/][/])
4, 5	bitr	6	([/][/])
2	sbco2w	7	([/][/][/])
7	eqt-∀-i	8	([/][/][/])
6, 8	<>bitr	9	([/])