Definition df-ad 132

Description: Plus is the dual of With.

Assertion

Ref	Expression
df-ad	⊦ ((𝜑 ⊕ 𝜓) ⧟ ~ (~ 𝜑 & ~ 𝜓))

Detailed syntax breakdown of Definition df-ad

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wad 131	. 2 wff (𝜑 ⊕ 𝜓)
4	1	wneg 3	. . . 4 wff ~ 𝜑
5	2	wneg 3	. . . 4 wff ~ 𝜓
6	4, 5	wac 30	. . 3 wff (~ 𝜑 & ~ 𝜓)
7	6	wneg 3	. 2 wff ~ (~ 𝜑 & ~ 𝜓)
8	3, 7	wlb 55	1 wff ((𝜑 ⊕ 𝜓) ⧟ ~ (~ 𝜑 & ~ 𝜓))

This definition is referenced by:  abs1  178