Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem oa63v 1011

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 270	. . . . 5 (a →₂c)^⊥ = (c^⊥ ∩ (a ∪ c))
2		lea 152	. . . . 5 (c^⊥ ∩ (a ∪ c)) ≤ c^⊥
3	1, 2	bltr 130	. . . 4 (a →₂c)^⊥ ≤ c^⊥
4		ud2lem0c 270	. . . . 5 (a →₂b)^⊥ = (b^⊥ ∩ (a ∪ b))
5		lea 152	. . . . 5 (b^⊥ ∩ (a ∪ b)) ≤ b^⊥
6	4, 5	bltr 130	. . . 4 (a →₂b)^⊥ ≤ b^⊥
7	3, 6	oa64v 1010	. . . 4 (((a →₂c)^⊥ ∪ c) ∩ ((a →₂b)^⊥ ∪ b)) ≤ (c ∪ ((a →₂c)^⊥ ∩ ((a →₂b)^⊥ ∪ (((a →₂c)^⊥ ∪ (a →₂b)^⊥ ) ∩ (c ∪ b)))))
8		id 58	. . . 4 (a →₂c)^⊥ = (a →₂c)^⊥
9		id 58	. . . 4 (a →₂b)^⊥ = (a →₂b)^⊥
10	3, 6, 7, 8, 9	oa4v3v 914	. . 3 (c^⊥ ∩ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))) ≤ ((c^⊥ ∩ (a →₂c)) ∪ (b^⊥ ∩ (a →₂b)))
11	10	oal42 915	. 2 (c^⊥ ∩ ((a →₂c) ∪ ((a →₂b) ∩ ((c ∪ b)^⊥ ∪ ((a →₂c) ∩ (a →₂b)))))) ≤ a^⊥
12	11	oa23 916	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 14

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 ax-oa6 1009

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