Axiom ax-nure 216

Description: Commutation of ν with ≫.

Assertion

Ref	Expression
ax-nure	⊦ (νx[u ≫ v] 𝜑 ⧟ [u ≫ v] νx𝜑)

Detailed syntax breakdown of Axiom ax-nure

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

This axiom is referenced by: (None)