Axiom ax-nuse 215

Description: Commutation of ν with ≪.

Assertion

Ref	Expression
ax-nuse	⊦ (νx[u ≪ v] 𝜑 ⧟ [u ≪ v] νx𝜑)

Detailed syntax breakdown of Axiom ax-nuse

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		vu	. . . . 5 var u
3	2	nvar 203	. . . 4 nilad u
4		vv	. . . . 5 var v
5	4	nvar 203	. . . 4 nilad v
6	1, 3, 5	wse 204	. . 3 wff [u ≪ v] 𝜑
7		vx	. . 3 var x
8	6, 7	wnu 206	. 2 wff νx[u ≪ v] 𝜑
9	1, 7	wnu 206	. . 3 wff νx𝜑
10	9, 3, 5	wse 204	. 2 wff [u ≪ v] νx𝜑
11	8, 10	wlb 55	1 wff (νx[u ≪ v] 𝜑 ⧟ [u ≪ v] νx𝜑)

This axiom is referenced by: (None)