Theorem dnid 23

Description: Double negation introduction.

Hypothesis

Ref	Expression
dnid.1	⊦ (𝜑 ⅋ 𝜓)

Assertion

Ref	Expression
dnid	⊦ (𝜑 ⅋ ~ ~ 𝜓)

Proof of Theorem dnid

Step	Hyp	Ref	Expression
1		dnid.1	. 2 ⊦ (𝜑 ⅋ 𝜓)
2		ax-init 7	. . 3 ⊦ (~ ~ 𝜓 ⅋ ~ 𝜓)
3	2	mdcoi 12	. 2 ⊦ (~ 𝜓 ⅋ ~ ~ 𝜓)
4	1, 3	ax-cut 6	1 ⊦ (𝜑 ⅋ ~ ~ 𝜓)

Syntax hints:   ⅋ wmd 2  ~ wneg 3

This theorem was proved from axioms:  ax-ibot 4  ax-ebot 5  ax-cut 6  ax-init 7  ax-mdco 8

This theorem is referenced by:  dned  24  dni1  25  licond  95  abs1  178