Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem elimcons2 851

Description: Consequent elimination law.

**Hypotheses**
Ref	Expression
elimcons2.1	(a →₁c) = (b →₁c)
elimcons2.2	(a ∩ (c ∩ (b →₁c))) ≤ (b ∪ (c^⊥ ∪ (a →₁c)^⊥ ))

**Assertion**
Ref	Expression
elimcons2	a ≤ b

**Proof of Theorem elimcons2**
Step	Hyp	Ref	Expression
1		elimcons2.1	. 2 (a →₁c) = (b →₁c)
2		elimcons2.2	. . 3 (a ∩ (c ∩ (b →₁c))) ≤ (b ∪ (c^⊥ ∪ (a →₁c)^⊥ ))
3	1	ax-r1 34	. . . . . . 7 (b →₁c) = (a →₁c)
4		df-i1 43	. . . . . . 7 (a →₁c) = (a^⊥ ∪ (a ∩ c))
5	3, 4	ax-r2 35	. . . . . 6 (b →₁c) = (a^⊥ ∪ (a ∩ c))
6	5	lan 70	. . . . 5 (c ∩ (b →₁c)) = (c ∩ (a^⊥ ∪ (a ∩ c)))
7	6	lan 70	. . . 4 (a ∩ (c ∩ (b →₁c))) = (a ∩ (c ∩ (a^⊥ ∪ (a ∩ c))))
8		anass 69	. . . . 5 ((a ∩ c) ∩ (a^⊥ ∪ (a ∩ c))) = (a ∩ (c ∩ (a^⊥ ∪ (a ∩ c))))
9	8	ax-r1 34	. . . 4 (a ∩ (c ∩ (a^⊥ ∪ (a ∩ c)))) = ((a ∩ c) ∩ (a^⊥ ∪ (a ∩ c)))
10		leor 151	. . . . 5 (a ∩ c) ≤ (a^⊥ ∪ (a ∩ c))
11	10	df2le2 128	. . . 4 ((a ∩ c) ∩ (a^⊥ ∪ (a ∩ c))) = (a ∩ c)
12	7, 9, 11	3tr 62	. . 3 (a ∩ (c ∩ (b →₁c))) = (a ∩ c)
13	1	ax-r4 36	. . . . . . . 8 (a →₁c)^⊥ = (b →₁c)^⊥
14		ud1lem0c 269	. . . . . . . 8 (b →₁c)^⊥ = (b ∩ (b^⊥ ∪ c^⊥ ))
15	13, 14	ax-r2 35	. . . . . . 7 (a →₁c)^⊥ = (b ∩ (b^⊥ ∪ c^⊥ ))
16	15	lor 66	. . . . . 6 (c^⊥ ∪ (a →₁c)^⊥ ) = (c^⊥ ∪ (b ∩ (b^⊥ ∪ c^⊥ )))
17		ax-a2 30	. . . . . 6 (c^⊥ ∪ (b ∩ (b^⊥ ∪ c^⊥ ))) = ((b ∩ (b^⊥ ∪ c^⊥ )) ∪ c^⊥ )
18	16, 17	ax-r2 35	. . . . 5 (c^⊥ ∪ (a →₁c)^⊥ ) = ((b ∩ (b^⊥ ∪ c^⊥ )) ∪ c^⊥ )
19	18	lor 66	. . . 4 (b ∪ (c^⊥ ∪ (a →₁c)^⊥ )) = (b ∪ ((b ∩ (b^⊥ ∪ c^⊥ )) ∪ c^⊥ ))
20		ax-a3 31	. . . . 5 ((b ∪ (b ∩ (b^⊥ ∪ c^⊥ ))) ∪ c^⊥ ) = (b ∪ ((b ∩ (b^⊥ ∪ c^⊥ )) ∪ c^⊥ ))
21	20	ax-r1 34	. . . 4 (b ∪ ((b ∩ (b^⊥ ∪ c^⊥ )) ∪ c^⊥ )) = ((b ∪ (b ∩ (b^⊥ ∪ c^⊥ ))) ∪ c^⊥ )
22		ax-a2 30	. . . . . 6 (b ∪ (b ∩ (b^⊥ ∪ c^⊥ ))) = ((b ∩ (b^⊥ ∪ c^⊥ )) ∪ b)
23		lea 152	. . . . . . 7 (b ∩ (b^⊥ ∪ c^⊥ )) ≤ b
24	23	df-le2 123	. . . . . 6 ((b ∩ (b^⊥ ∪ c^⊥ )) ∪ b) = b
25	22, 24	ax-r2 35	. . . . 5 (b ∪ (b ∩ (b^⊥ ∪ c^⊥ ))) = b
26	25	ax-r5 37	. . . 4 ((b ∪ (b ∩ (b^⊥ ∪ c^⊥ ))) ∪ c^⊥ ) = (b ∪ c^⊥ )
27	19, 21, 26	3tr 62	. . 3 (b ∪ (c^⊥ ∪ (a →₁c)^⊥ )) = (b ∪ c^⊥ )
28	2, 12, 27	le3tr2 133	. 2 (a ∩ c) ≤ (b ∪ c^⊥ )
29	1, 28	elimcons 850	1 a ≤ b

Colors of variables: term

Syntax hints: = wb 1 ≤ wle 2 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 →₁wi1 13

This theorem was proved from axioms: ax-a1 29 ax-a2 30 ax-a3 31 ax-a4 32 ax-a5 33 ax-r1 34 ax-r2 35 ax-r4 36 ax-r5 37 ax-r3 421

This theorem depends on definitions: df-b 38 df-a 39 df-t 40 df-f 41 df-i1 43 df-le1 122 df-le2 123 df-c1 124 df-c2 125

metamath.org