Axiom ax-alcom 331

Description: Quantifier commutation.

Assertion

Ref	Expression
ax-alcom	⊦ (∀x∀y𝜑 ⊸ ∀y∀x𝜑)

Detailed syntax breakdown of Axiom ax-alcom

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		vy	. . . 4 var y
3	1, 2	wal 318	. . 3 wff ∀y𝜑
4		vx	. . 3 var x
5	3, 4	wal 318	. 2 wff ∀x∀y𝜑
6	1, 4	wal 318	. . 3 wff ∀x𝜑
7	6, 2	wal 318	. 2 wff ∀y∀x𝜑
8	5, 7	wli 61	1 wff (∀x∀y𝜑 ⊸ ∀y∀x𝜑)

This axiom is referenced by: (None)