Definition df-not 187

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

Assertion

Ref	Expression
df-not	⊦ (¬ 𝜑 ⧟ ~ ! 𝜑)

Detailed syntax breakdown of Definition df-not

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2	1	wnot 186	. 2 wff ¬ 𝜑
3	1	wpe 148	. . 3 wff ! 𝜑
4	3	wneg 3	. 2 wff ~ ! 𝜑
5	2, 4	wlb 55	1 wff (¬ 𝜑 ⧟ ~ ! 𝜑)

This definition is referenced by: (None)