Definition df-and 183

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

Assertion

Ref	Expression
df-and	⊦ ((𝜑 ∧ 𝜓) ⧟ (! 𝜑 & ! 𝜓))

Detailed syntax breakdown of Definition df-and

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wand 182	. 2 wff (𝜑 ∧ 𝜓)
4	1	wpe 148	. . 3 wff ! 𝜑
5	2	wpe 148	. . 3 wff ! 𝜓
6	4, 5	wac 30	. 2 wff (! 𝜑 & ! 𝜓)
7	3, 6	wlb 55	1 wff ((𝜑 ∧ 𝜓) ⧟ (! 𝜑 & ! 𝜓))

This definition is referenced by: (None)