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

---

Theorem dp41lemc0 1182

Description: Part of proof (4)=>(1) in Day/Pickering 1982.

Hypotheses

Ref	Expression
dp41lem.1	c0 a1 a2 b1 b2
dp41lem.2	c1 a0 a2 b0 b2
dp41lem.3	c2 a0 a1 b0 b1
dp41lem.4	a0 b0 a1 b1 a2 b2
dp41lem.5	p2 a0 b0 a1 b1
dp41lem.6	p2 a2 b2

Assertion

Ref	Expression
dp41lemc0	a0 b0 b1 a0 a1 b1 a0 b1 a0 b0 a1 b1

---

Proof of Theorem dp41lemc0

Step	Hyp	Ref	Expression
1		ax-a2 31	. . . . . . 7 a0 a1 a1 a0
2	1	ror 71	. . . . . 6 a0 a1 b1 a1 a0 b1
3		or32 82	. . . . . 6 a1 a0 b1 a1 b1 a0
4	2, 3	tr 62	. . . . 5 a0 a1 b1 a1 b1 a0
5	4	lan 77	. . . 4 a0 b0 b1 a0 a1 b1 a0 b0 b1 a1 b1 a0
6		ancom 74	. . . 4 a0 b0 b1 a1 b1 a0 a1 b1 a0 a0 b0 b1
7	5, 6	tr 62	. . 3 a0 b0 b1 a0 a1 b1 a1 b1 a0 a0 b0 b1
8		leor 159	. . . . 5 b1 a1 b1
9	8	ler 149	. . . 4 b1 a1 b1 a0
10	9	mldual2i 1125	. . 3 a1 b1 a0 a0 b0 b1 a1 b1 a0 a0 b0 b1
11		ancom 74	. . . . 5 a1 b1 a0 a0 b0 a0 b0 a1 b1 a0
12		leo 158	. . . . . 6 a0 a0 b0
13	12	mldual2i 1125	. . . . 5 a0 b0 a1 b1 a0 a0 b0 a1 b1 a0
14	11, 13	tr 62	. . . 4 a1 b1 a0 a0 b0 a0 b0 a1 b1 a0
15	14	ror 71	. . 3 a1 b1 a0 a0 b0 b1 a0 b0 a1 b1 a0 b1
16	7, 10, 15	3tr 65	. 2 a0 b0 b1 a0 a1 b1 a0 b0 a1 b1 a0 b1
17		orass 75	. 2 a0 b0 a1 b1 a0 b1 a0 b0 a1 b1 a0 b1
18		orcom 73	. 2 a0 b0 a1 b1 a0 b1 a0 b1 a0 b0 a1 b1
19	16, 17, 18	3tr 65	1 a0 b0 b1 a0 a1 b1 a0 b1 a0 b0 a1 b1

Colors of variables: term

Syntax hints:   wb 1   wle 2   wo 6   wa 7

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-ml 1120

This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is referenced by:  dp41lemc  1183

Copyright terms: Public domain

W3C validator