oi3oa3 - Quantum Logic Explorer

	Quantum Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > QLE Home > Th. List > oi3oa3		GIF version

Theorem oi3oa3 733

Description: An attempt at the OA3 conjecture, which is true if (a ≡ b) = 1. (Contributed by Josiah Burroughs, 27-May-2004.)

**Hypothesis**
Ref	Expression
oi3oa3.1	1 = (b ≡ a)

**Assertion**
Ref	Expression
oi3oa3	(((a →₁c) ∩ (b →₁c)) ∪ ((((a →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c) ∩ (((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c))) = 1

**Proof of Theorem oi3oa3**
Step	Hyp	Ref	Expression
1		oi3oa3.1	. . . . . . . 8 1 = (b ≡ a)
2	1	oi3oa3lem1 732	. . . . . . 7 (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b)) = 1
3	2	lan 77	. . . . . 6 ((a →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) = ((a →₁c) ∩ 1)
4		an1 106	. . . . . 6 ((a →₁c) ∩ 1) = (a →₁c)
5	3, 4	ax-r2 36	. . . . 5 ((a →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) = (a →₁c)
6	5	ud1lem0b 256	. . . 4 (((a →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c) = ((a →₁c) →₁c)
7	2	lan 77	. . . . . 6 ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) = ((b →₁c) ∩ 1)
8		an1 106	. . . . . 6 ((b →₁c) ∩ 1) = (b →₁c)
9	7, 8	ax-r2 36	. . . . 5 ((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) = (b →₁c)
10	9	ud1lem0b 256	. . . 4 (((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c) = ((b →₁c) →₁c)
11	6, 10	2an 79	. . 3 ((((a →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c) ∩ (((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c)) = (((a →₁c) →₁c) ∩ ((b →₁c) →₁c))
12	11	lor 70	. 2 (((a →₁c) ∩ (b →₁c)) ∪ ((((a →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c) ∩ (((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c))) = (((a →₁c) ∩ (b →₁c)) ∪ (((a →₁c) →₁c) ∩ ((b →₁c) →₁c)))
13		ax-a2 31	. 2 (((a →₁c) ∩ (b →₁c)) ∪ (((a →₁c) →₁c) ∩ ((b →₁c) →₁c))) = ((((a →₁c) →₁c) ∩ ((b →₁c) →₁c)) ∪ ((a →₁c) ∩ (b →₁c)))
14	1	r3a 440	. . . . 5 b = a
15	14	ud1lem0b 256	. . . 4 (b →₁c) = (a →₁c)
16	15	1bi 119	. . 3 1 = ((b →₁c) ≡ (a →₁c))
17	16	oi3oa3lem1 732	. 2 ((((a →₁c) →₁c) ∩ ((b →₁c) →₁c)) ∪ ((a →₁c) ∩ (b →₁c))) = 1
18	12, 13, 17	3tr 65	1 (((a →₁c) ∩ (b →₁c)) ∪ ((((a →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c) ∩ (((b →₁c) ∩ (((a →₁c) ∩ (b →₁c)) ∪ (a ∩ b))) →₁c))) = 1

Colors of variables: term

Syntax hints: = wb 1 ≡ tb 5 ∪ wo 6 ∩ wa 7 1wt 8 →₁wi1 12

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

This theorem depends on definitions: df-b 39 df-a 40 df-t 41 df-f 42 df-i1 44

This theorem is referenced by: (None)

W3C validator