Theorem ebotr 19

Description: Remove a ⊥, right hand side. See ax-ebot 5.

Hypothesis

Ref	Expression
ebotr.1	⊦ (𝜑 ⅋ ⊥)

Assertion

Ref	Expression
ebotr	⊦ 𝜑

Proof of Theorem ebotr

Step	Hyp	Ref	Expression
1		ebotr.1	. . 3 ⊦ (𝜑 ⅋ ⊥)
2	1	mdcoi 12	. 2 ⊦ (⊥ ⅋ 𝜑)
3	2	ax-ebot 5	1 ⊦ 𝜑

Syntax hints:  ⊥wbot 1   ⅋ wmd 2

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

This theorem is referenced by:  nebot  20  md1  113