Axiom ax-numc 218

Description: Commutation of ν into ⊗. Note that x can only be bound in one factor.

Assertion

Ref	Expression
ax-numc	⊦ (νx(𝜑 ⊗ νx𝜓) ⧟ (νx𝜑 ⊗ νx𝜓))

Detailed syntax breakdown of Axiom ax-numc

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		wps	. . . . 5 wff 𝜓
3		vx	. . . . 5 var x
4	2, 3	wnu 206	. . . 4 wff νx𝜓
5	1, 4	wmc 105	. . 3 wff (𝜑 ⊗ νx𝜓)
6	5, 3	wnu 206	. 2 wff νx(𝜑 ⊗ νx𝜓)
7	1, 3	wnu 206	. . 3 wff νx𝜑
8	7, 4	wmc 105	. 2 wff (νx𝜑 ⊗ νx𝜓)
9	6, 8	wlb 55	1 wff (νx(𝜑 ⊗ νx𝜓) ⧟ (νx𝜑 ⊗ νx𝜓))

This axiom is referenced by: (None)