Theorem dned 24

Description: Double negation elimination.

Hypothesis

Ref	Expression
dned.1	⊦ (𝜑 ⅋ ~ ~ 𝜓)

Assertion

Ref	Expression
dned	⊦ (𝜑 ⅋ 𝜓)

Proof of Theorem dned

Step	Hyp	Ref	Expression
1		dned.1	. 2 ⊦ (𝜑 ⅋ ~ ~ 𝜓)
2		ax-init 7	. . . . 5 ⊦ (~ 𝜓 ⅋ 𝜓)
3	2	mdcoi 12	. . . 4 ⊦ (𝜓 ⅋ ~ 𝜓)
4	3	dnid 23	. . 3 ⊦ (𝜓 ⅋ ~ ~ ~ 𝜓)
5	4	mdcoi 12	. 2 ⊦ (~ ~ ~ 𝜓 ⅋ 𝜓)
6	1, 5	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:  dne1  26  abs1  178