oa63v - Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem oa63v 1031

Description: Derivation of 3-variable OA from 6-variable OA.

**Assertion**
Ref	Expression
oa63v	((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) ≤ (a →₂c)

**Proof of Theorem oa63v**
Step	Hyp	Ref	Expression
1		ud2lem0c 278	. . . . 5 (a →₂c)^⊥ = (c^⊥ ∩ (a ∪ c))
2		lea 160	. . . . 5 (c^⊥ ∩ (a ∪ c)) ≤ c^⊥
3	1, 2	bltr 138	. . . 4 (a →₂c)^⊥ ≤ c^⊥
4		ud2lem0c 278	. . . . 5 (a →₂b)^⊥ = (b^⊥ ∩ (a ∪ b))
5		lea 160	. . . . 5 (b^⊥ ∩ (a ∪ b)) ≤ b^⊥
6	4, 5	bltr 138	. . . 4 (a →₂b)^⊥ ≤ b^⊥
7	3, 6	oa64v 1030	. . . 4 (((a →₂c)^⊥ ∪ c) ∩ ((a →₂b)^⊥ ∪ b)) ≤ (c ∪ ((a →₂c)^⊥ ∩ ((a →₂b)^⊥ ∪ (((a →₂c)^⊥ ∪ (a →₂b)^⊥ ) ∩ (c ∪ b)))))
8		id 59	. . . 4 (a →₂c)^⊥ = (a →₂c)^⊥
9		id 59	. . . 4 (a →₂b)^⊥ = (a →₂b)^⊥
10	3, 6, 7, 8, 9	oa4v3v 934	. . 3 (c^⊥ ∩ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))) ≤ ((c^⊥ ∩ (a →₂c)) ∪ (b^⊥ ∩ (a →₂b)))
11	10	oal42 935	. 2 (c^⊥ ∩ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))) ≤ a^⊥
12	11	oa23 936	1 ((a →₂b) ∩ ((b ∪ c)^⊥ ∪ ((a →₂b) ∩ (a →₂c)))) ≤ (a →₂c)

Colors of variables: term

Syntax hints: ≤ wle 2 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 →₂wi2 13

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

This theorem depends on definitions: df-b 39 df-a 40 df-t 41 df-f 42 df-i2 45 df-le1 130 df-le2 131 df-c1 132 df-c2 133