Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem 3vth6 791

Description: A 3-variable theorem.

**Assertion**
Ref	Expression
3vth6	((a →₂b)^⊥ →₂(b ∪ c)) = (((a →₂b) ∩ (c →₂b)) ∪ ((a →₂c) ∩ (b →₂c)))

**Proof of Theorem 3vth6**
Step	Hyp	Ref	Expression
1		oridm 102	. . 3 (((a →₂b)^⊥ →₂(b ∪ c)) ∪ ((a →₂b)^⊥ →₂(b ∪ c))) = ((a →₂b)^⊥ →₂(b ∪ c))
2	1	ax-r1 34	. 2 ((a →₂b)^⊥ →₂(b ∪ c)) = (((a →₂b)^⊥ →₂(b ∪ c)) ∪ ((a →₂b)^⊥ →₂(b ∪ c)))
3		3vth4 789	. . . 4 ((a →₂b)^⊥ →₂(b ∪ c)) = ((a →₂c)^⊥ →₂(b ∪ c))
4	3	lor 66	. . 3 (((a →₂b)^⊥ →₂(b ∪ c)) ∪ ((a →₂b)^⊥ →₂(b ∪ c))) = (((a →₂b)^⊥ →₂(b ∪ c)) ∪ ((a →₂c)^⊥ →₂(b ∪ c)))
5		3vth5 790	. . . . 5 ((a →₂b)^⊥ →₂(b ∪ c)) = (c ∪ ((a →₂b) ∩ (c →₂b)))
6		ax-a2 30	. . . . . . 7 (b ∪ c) = (c ∪ b)
7	6	ud2lem0a 250	. . . . . 6 ((a →₂c)^⊥ →₂(b ∪ c)) = ((a →₂c)^⊥ →₂(c ∪ b))
8		3vth5 790	. . . . . 6 ((a →₂c)^⊥ →₂(c ∪ b)) = (b ∪ ((a →₂c) ∩ (b →₂c)))
9	7, 8	ax-r2 35	. . . . 5 ((a →₂c)^⊥ →₂(b ∪ c)) = (b ∪ ((a →₂c) ∩ (b →₂c)))
10	5, 9	2or 67	. . . 4 (((a →₂b)^⊥ →₂(b ∪ c)) ∪ ((a →₂c)^⊥ →₂(b ∪ c))) = ((c ∪ ((a →₂b) ∩ (c →₂b))) ∪ (b ∪ ((a →₂c) ∩ (b →₂c))))
11		or4 77	. . . . 5 ((c ∪ ((a →₂b) ∩ (c →₂b))) ∪ (b ∪ ((a →₂c) ∩ (b →₂c)))) = ((c ∪ b) ∪ (((a →₂b) ∩ (c →₂b)) ∪ ((a →₂c) ∩ (b →₂c))))
12		ax-a2 30	. . . . . . 7 (c ∪ b) = (b ∪ c)
13	12	ax-r5 37	. . . . . 6 ((c ∪ b) ∪ (((a →₂b) ∩ (c →₂b)) ∪ ((a →₂c) ∩ (b →₂c)))) = ((b ∪ c) ∪ (((a →₂b) ∩ (c →₂b)) ∪ ((a →₂c) ∩ (b →₂c))))
14		or4 77	. . . . . . 7 ((b ∪ c) ∪ (((a →₂b) ∩ (c →₂b)) ∪ ((a →₂c) ∩ (b →₂c)))) = ((b ∪ ((a →₂b) ∩ (c →₂b))) ∪ (c ∪ ((a →₂c) ∩ (b →₂c))))
15		leo 150	. . . . . . . . . . 11 b ≤ (b ∪ (a^⊥ ∩ b^⊥ ))
16		df-i2 44	. . . . . . . . . . . 12 (a →₂b) = (b ∪ (a^⊥ ∩ b^⊥ ))
17	16	ax-r1 34	. . . . . . . . . . 11 (b ∪ (a^⊥ ∩ b^⊥ )) = (a →₂b)
18	15, 17	lbtr 131	. . . . . . . . . 10 b ≤ (a →₂b)
19		leo 150	. . . . . . . . . . 11 b ≤ (b ∪ (c^⊥ ∩ b^⊥ ))
20		df-i2 44	. . . . . . . . . . . 12 (c →₂b) = (b ∪ (c^⊥ ∩ b^⊥ ))
21	20	ax-r1 34	. . . . . . . . . . 11 (b ∪ (c^⊥ ∩ b^⊥ )) = (c →₂b)
22	19, 21	lbtr 131	. . . . . . . . . 10 b ≤ (c →₂b)
23	18, 22	ler2an 165	. . . . . . . . 9 b ≤ ((a →₂b) ∩ (c →₂b))
24	23	df-le2 123	. . . . . . . 8 (b ∪ ((a →₂b) ∩ (c →₂b))) = ((a →₂b) ∩ (c →₂b))
25		leo 150	. . . . . . . . . . 11 c ≤ (c ∪ (a^⊥ ∩ c^⊥ ))
26		df-i2 44	. . . . . . . . . . . 12 (a →₂c) = (c ∪ (a^⊥ ∩ c^⊥ ))
27	26	ax-r1 34	. . . . . . . . . . 11 (c ∪ (a^⊥ ∩ c^⊥ )) = (a →₂c)
28	25, 27	lbtr 131	. . . . . . . . . 10 c ≤ (a →₂c)
29		leo 150	. . . . . . . . . . 11 c ≤ (c ∪ (b^⊥ ∩ c^⊥ ))
30		df-i2 44	. . . . . . . . . . . 12 (b →₂c) = (c ∪ (b^⊥ ∩ c^⊥ ))
31	30	ax-r1 34	. . . . . . . . . . 11 (c ∪ (b^⊥ ∩ c^⊥ )) = (b →₂c)
32	29, 31	lbtr 131	. . . . . . . . . 10 c ≤ (b →₂c)
33	28, 32	ler2an 165	. . . . . . . . 9 c ≤ ((a →₂c) ∩ (b →₂c))
34	33	df-le2 123	. . . . . . . 8 (c ∪ ((a →₂c) ∩ (b →₂c))) = ((a →₂c) ∩ (b →₂c))
35	24, 34	2or 67	. . . . . . 7 ((b ∪ ((a →₂b) ∩ (c →₂b))) ∪ (c ∪ ((a →₂c) ∩ (b →₂c)))) = (((a →₂b) ∩ (c →₂b)) ∪ ((a →₂c) ∩ (b →₂c)))
36	14, 35	ax-r2 35	. . . . . 6 ((b ∪ c) ∪ (((a →₂b) ∩ (c →₂b)) ∪ ((a →₂c) ∩ (b →₂c)))) = (((a →₂b) ∩ (c →₂b)) ∪ ((a →₂c) ∩ (b →₂c)))
37	13, 36	ax-r2 35	. . . . 5 ((c ∪ b) ∪ (((a →₂b) ∩ (c →₂b)) ∪ ((a →₂c) ∩ (b →₂c)))) = (((a →₂b) ∩ (c →₂b)) ∪ ((a →₂c) ∩ (b →₂c)))
38	11, 37	ax-r2 35	. . . 4 ((c ∪ ((a →₂b) ∩ (c →₂b))) ∪ (b ∪ ((a →₂c) ∩ (b →₂c)))) = (((a →₂b) ∩ (c →₂b)) ∪ ((a →₂c) ∩ (b →₂c)))
39	10, 38	ax-r2 35	. . 3 (((a →₂b)^⊥ →₂(b ∪ c)) ∪ ((a →₂c)^⊥ →₂(b ∪ c))) = (((a →₂b) ∩ (c →₂b)) ∪ ((a →₂c) ∩ (b →₂c)))
40	4, 39	ax-r2 35	. 2 (((a →₂b)^⊥ →₂(b ∪ c)) ∪ ((a →₂b)^⊥ →₂(b ∪ c))) = (((a →₂b) ∩ (c →₂b)) ∪ ((a →₂c) ∩ (b →₂c)))
41	2, 40	ax-r2 35	1 ((a →₂b)^⊥ →₂(b ∪ c)) = (((a →₂b) ∩ (c →₂b)) ∪ ((a →₂c) ∩ (b →₂c)))

Colors of variables: term

Syntax hints: = wb 1 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 →₂wi2 14

This theorem is referenced by: 3vth8 793

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-i2 44 df-le1 122 df-le2 123 df-c1 124 df-c2 125

metamath.org