Theorem abs1 178

Description: Absorption of Plus into With. Together with abs2 179, this shows the additive operators form a lattice.

Assertion

Ref	Expression
abs1	⊦ ((𝜑 ⊕ (𝜑 & 𝜓)) ⧟ 𝜑)

Proof of Theorem abs1

Step	Hyp	Ref	Expression
1		df-ad 132	. . . . 5 ⊦ ((𝜑 ⊕ (𝜑 & 𝜓)) ⧟ ~ (~ 𝜑 & ~ (𝜑 & 𝜓)))
2	1	lbi1 89	. . . 4 ⊦ ((𝜑 ⊕ (𝜑 & 𝜓)) ⊸ ~ (~ 𝜑 & ~ (𝜑 & 𝜓)))
3		ax-init 7	. . . . . . . . 9 ⊦ (~ ~ 𝜑 ⅋ ~ 𝜑)
4		ax-init 7	. . . . . . . . . . . 12 ⊦ (~ (𝜑 & 𝜓) ⅋ (𝜑 & 𝜓))
5	4	ax-eac1 33	. . . . . . . . . . 11 ⊦ (~ (𝜑 & 𝜓) ⅋ 𝜑)
6	5	dnid 23	. . . . . . . . . 10 ⊦ (~ (𝜑 & 𝜓) ⅋ ~ ~ 𝜑)
7	6	mdcoi 12	. . . . . . . . 9 ⊦ (~ ~ 𝜑 ⅋ ~ (𝜑 & 𝜓))
8	3, 7	ax-iac 32	. . . . . . . 8 ⊦ (~ ~ 𝜑 ⅋ (~ 𝜑 & ~ (𝜑 & 𝜓)))
9	8	dnid 23	. . . . . . 7 ⊦ (~ ~ 𝜑 ⅋ ~ ~ (~ 𝜑 & ~ (𝜑 & 𝜓)))
10	9	mdcoi 12	. . . . . 6 ⊦ (~ ~ (~ 𝜑 & ~ (𝜑 & 𝜓)) ⅋ ~ ~ 𝜑)
11	10	dned 24	. . . . 5 ⊦ (~ ~ (~ 𝜑 & ~ (𝜑 & 𝜓)) ⅋ 𝜑)
12	11	dfli2i 66	. . . 4 ⊦ (~ (~ 𝜑 & ~ (𝜑 & 𝜓)) ⊸ 𝜑)
13	2, 12	syl 75	. . 3 ⊦ ((𝜑 ⊕ (𝜑 & 𝜓)) ⊸ 𝜑)
14		ax-init 7	. . . . . . 7 ⊦ (~ (~ 𝜑 & ~ (𝜑 & 𝜓)) ⅋ (~ 𝜑 & ~ (𝜑 & 𝜓)))
15	14	eac1d 37	. . . . . 6 ⊦ (~ (~ 𝜑 & ~ (𝜑 & 𝜓)) ⅋ ~ 𝜑)
16	15	mdcoi 12	. . . . 5 ⊦ (~ 𝜑 ⅋ ~ (~ 𝜑 & ~ (𝜑 & 𝜓)))
17	16	dfli2i 66	. . . 4 ⊦ (𝜑 ⊸ ~ (~ 𝜑 & ~ (𝜑 & 𝜓)))
18	17, 1	lb2s 68	. . 3 ⊦ (𝜑 ⊸ (𝜑 ⊕ (𝜑 & 𝜓)))
19	13, 18	iaci 36	. 2 ⊦ (((𝜑 ⊕ (𝜑 & 𝜓)) ⊸ 𝜑) & (𝜑 ⊸ (𝜑 ⊕ (𝜑 & 𝜓))))
20		dflb 93	. 2 ⊦ (((𝜑 ⊕ (𝜑 & 𝜓)) ⧟ 𝜑) ⧟ (((𝜑 ⊕ (𝜑 & 𝜓)) ⊸ 𝜑) & (𝜑 ⊸ (𝜑 ⊕ (𝜑 & 𝜓)))))
21	19, 20	lb2i 60	1 ⊦ ((𝜑 ⊕ (𝜑 & 𝜓)) ⧟ 𝜑)

Syntax hints:  ~ wneg 3   & wac 30   ⧟ wlb 55   ⊸ wli 61   ⊕ wad 131

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  df-ad 132

This theorem is referenced by: (None)