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	⊢ [ 𝑥 ⇄ 𝑦 ] ∀ 𝑥 ∀ 𝑦 𝜑

Proof

Step	Hyp	Ref	Expression
1		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∀ 𝑦 𝜑
2		nfa2	⊢ Ⅎ 𝑦 ∀ 𝑥 ∀ 𝑦 𝜑
3	1 2	ichf	⊢ [ 𝑥 ⇄ 𝑦 ] ∀ 𝑥 ∀ 𝑦 𝜑