Axiom ax-nunu 219

Description: Commutation of ν with ν. There is no need for a distinct variable condition on x and y, since (νxνx𝜑 ⧟ νxνx𝜑) is a valid theorem.

Assertion

Ref	Expression
ax-nunu	⊦ (νxνy𝜑 ⧟ νyνx𝜑)

Detailed syntax breakdown of Axiom ax-nunu

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		vy	. . . 4 var y
3	1, 2	wnu 206	. . 3 wff νy𝜑
4		vx	. . 3 var x
5	3, 4	wnu 206	. 2 wff νxνy𝜑
6	1, 4	wnu 206	. . 3 wff νx𝜑
7	6, 2	wnu 206	. 2 wff νyνx𝜑
8	5, 7	wlb 55	1 wff (νxνy𝜑 ⧟ νyνx𝜑)

This axiom is referenced by: (None)