Theorem md1 113

Description: ⊥ is the unit of ⅋ (left side).

Assertion

Ref	Expression
md1	⊦ (𝜑 ⧟ (⊥ ⅋ 𝜑))

Proof of Theorem md1

Step	Hyp	Ref	Expression
1		ax-init 7	. . . . . . 7 ⊦ (~ 𝜑 ⅋ 𝜑)
2	1	ax-ibot 4	. . . . . 6 ⊦ (⊥ ⅋ (~ 𝜑 ⅋ 𝜑))
3	2	mdcoi 12	. . . . 5 ⊦ ((~ 𝜑 ⅋ 𝜑) ⅋ ⊥)
4	3	mdasi 14	. . . 4 ⊦ (~ 𝜑 ⅋ (𝜑 ⅋ ⊥))
5	4	mdcod 11	. . 3 ⊦ (~ 𝜑 ⅋ (⊥ ⅋ 𝜑))
6	5	dfli2i 66	. 2 ⊦ (𝜑 ⊸ (⊥ ⅋ 𝜑))
7		ax-init 7	. . . . . 6 ⊦ (~ (⊥ ⅋ 𝜑) ⅋ (⊥ ⅋ 𝜑))
8	7	mdcod 11	. . . . 5 ⊦ (~ (⊥ ⅋ 𝜑) ⅋ (𝜑 ⅋ ⊥))
9	8	mdasri 17	. . . 4 ⊦ ((~ (⊥ ⅋ 𝜑) ⅋ 𝜑) ⅋ ⊥)
10	9	ebotr 19	. . 3 ⊦ (~ (⊥ ⅋ 𝜑) ⅋ 𝜑)
11	10	dfli2i 66	. 2 ⊦ ((⊥ ⅋ 𝜑) ⊸ 𝜑)
12	6, 11	ilb 96	1 ⊦ (𝜑 ⧟ (⊥ ⅋ 𝜑))

Syntax hints:  ⊥wbot 1   ⅋ wmd 2  ~ wneg 3   ⧟ wlb 55

This theorem was proved from axioms:  ax-ibot 4  ax-ebot 5  ax-cut 6  ax-init 7  ax-mdco 8  ax-mdas 9  ax-iac 32  ax-eac1 33  ax-eac2 34

This theorem depends on definitions:  df-lb 56  df-li 62

This theorem is referenced by:  md2  114