Axiom ax-nuad 217

Description: Distribution of ν over ⊕.

Assertion

Ref	Expression
ax-nuad	⊦ (νx(𝜑 ⊕ 𝜓) ⧟ (νx𝜑 ⊕ νx𝜓))

Detailed syntax breakdown of Axiom ax-nuad

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

This axiom is referenced by: (None)