Theorem ich2al

Description: Two setvar variables are always interchangeable when there are two universal quantifiers. (Contributed by SN, 23-Nov-2023)

	Ref	Expression
Assertion	ich2al	$$⊢\left[x\rightleftarrows y\right]\forall x\forall y\phi$$

Proof

Step	Hyp	Ref	Expression
1		nfa1	$$⊢Ⅎx\forall x\forall y\phi$$
2		nfa2	$$⊢Ⅎy\forall x\forall y\phi$$
3	1 2	ichf	$$⊢\left[x\rightleftarrows y\right]\forall x\forall y\phi$$