Definition df-mc 106

Description: Times is the dual of Par.

Assertion

Ref	Expression
df-mc	⊦ ((𝜑 ⊗ 𝜓) ⧟ ~ (~ 𝜑 ⅋ ~ 𝜓))

Detailed syntax breakdown of Definition df-mc

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wmc 105	. 2 wff (𝜑 ⊗ 𝜓)
4	1	wneg 3	. . . 4 wff ~ 𝜑
5	2	wneg 3	. . . 4 wff ~ 𝜓
6	4, 5	wmd 2	. . 3 wff (~ 𝜑 ⅋ ~ 𝜓)
7	6	wneg 3	. 2 wff ~ (~ 𝜑 ⅋ ~ 𝜓)
8	3, 7	wlb 55	1 wff ((𝜑 ⊗ 𝜓) ⧟ ~ (~ 𝜑 ⅋ ~ 𝜓))

This definition is referenced by:  mcco  115