Axiom ax-L11 28

Description: Quantifier Commutation.

Assertion

Ref	Expression
ax-L11	⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Axiom ax-L11

Step	Hyp	Ref	Expression
1		wff-ph	. . . 4 wff 𝜑
2		objvar-y	. . . 4 objvar 𝑦
3	1, 2	wff-forall 8	. . 3 wff ∀𝑦𝜑
4		objvar-x	. . 3 objvar 𝑥
5	3, 4	wff-forall 8	. 2 wff ∀𝑥∀𝑦𝜑
6	1, 4	wff-forall 8	. . 3 wff ∀𝑥𝜑
7	6, 2	wff-forall 8	. 2 wff ∀𝑦∀𝑥𝜑
8	5, 7	wff-imp 10	1 wff (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)

This axiom is referenced by:  allcomm-P6  739