Definition df-or 185

Description: Definition of ∨. It's ⊕ but with some ! splashed in for good measure.

Assertion

Ref	Expression
df-or	⊦ ((𝜑 ∨ 𝜓) ⧟ (! 𝜑 ⊕ ! 𝜓))

Detailed syntax breakdown of Definition df-or

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wor 184	. 2 wff (𝜑 ∨ 𝜓)
4	1	wpe 148	. . 3 wff ! 𝜑
5	2	wpe 148	. . 3 wff ! 𝜓
6	4, 5	wad 131	. 2 wff (! 𝜑 ⊕ ! 𝜓)
7	3, 6	wlb 55	1 wff ((𝜑 ∨ 𝜓) ⧟ (! 𝜑 ⊕ ! 𝜓))

This definition is referenced by: (None)