Theorem nebot 20

Description: Infer ~ ⊥ (secretly 1).

Assertion

Ref	Expression
nebot	⊦ ~ ⊥

Proof of Theorem nebot

Step	Hyp	Ref	Expression
1		ax-init 7	. 2 ⊦ (~ ⊥ ⅋ ⊥)
2	1	ebotr 19	1 ⊦ ~ ⊥

Syntax hints:  ⊥wbot 1  ~ 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: (None)