Theorem inenebot 27

Description: Add a ~ ~ ⊥. See ax-ibot 4. This is useful for dealing with deductions where the antecedent is negated.

Hypothesis

Ref	Expression
inenebot.1	⊦ 𝜑

Assertion

Ref	Expression
inenebot	⊦ (~ ~ ⊥ ⅋ 𝜑)

Proof of Theorem inenebot

Step	Hyp	Ref	Expression
1		inenebot.1	. . 3 ⊦ 𝜑
2	1	ax-ibot 4	. 2 ⊦ (⊥ ⅋ 𝜑)
3	2	dni1 25	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