Theorem ibotr 18

Description: Add a ⊥, right hand side. See ax-ibot 4.

Hypothesis

Ref	Expression
ibotr.1	⊦ 𝜑

Assertion

Ref	Expression
ibotr	⊦ (𝜑 ⅋ ⊥)

Proof of Theorem ibotr

Step	Hyp	Ref	Expression
1		ibotr.1	. . 3 ⊦ 𝜑
2	1	ax-ibot 4	. 2 ⊦ (⊥ ⅋ 𝜑)
3	2	mdcoi 12	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: (None)