Theorem enenebot 28

Description: Remove a ~ ~ ⊥. Inverse of inenebot 27.

Hypothesis

Ref	Expression
enenebot.1	⊦ (~ ~ ⊥ ⅋ 𝜑)

Assertion

Ref	Expression
enenebot	⊦ 𝜑

Proof of Theorem enenebot

Step	Hyp	Ref	Expression
1		enenebot.1	. . 3 ⊦ (~ ~ ⊥ ⅋ 𝜑)
2	1	dne1 26	. 2 ⊦ (⊥ ⅋ 𝜑)
3	2	ax-ebot 5	1 ⊦ 𝜑

Syntax hints:  ⊥wbot 1   ⅋ 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:  eac1i  38  eac2i  40