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

---

Theorem dp41leme 1185

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
dp41leme	c2 c0 c1 c2 a0 b1 c0 c1 a0 b0 b1 b1 a0 a1

---

Proof of Theorem dp41leme

Step	Hyp	Ref	Expression
1		mldual 1122	. . 3 c2 c0 c1 c2 a0 b1 c2 c0 c1 c2 a0 b1
2		dp41lem.3	. . . . . 6 c2 a0 a1 b0 b1
3	2	ran 78	. . . . 5 c2 a0 b1 a0 a1 b0 b1 a0 b1
4		anass 76	. . . . 5 a0 a1 b0 b1 a0 b1 a0 a1 b0 b1 a0 b1
5		leor 159	. . . . . . . . 9 b1 b0 b1
6	5	mldual2i 1125	. . . . . . . 8 b0 b1 a0 b1 b0 b1 a0 b1
7		orcom 73	. . . . . . . 8 b0 b1 a0 b1 b1 b0 b1 a0
8		ancom 74	. . . . . . . . 9 b0 b1 a0 a0 b0 b1
9	8	lor 70	. . . . . . . 8 b1 b0 b1 a0 b1 a0 b0 b1
10	6, 7, 9	3tr 65	. . . . . . 7 b0 b1 a0 b1 b1 a0 b0 b1
11	10	lan 77	. . . . . 6 a0 a1 b0 b1 a0 b1 a0 a1 b1 a0 b0 b1
12		leao1 162	. . . . . . 7 a0 b0 b1 a0 a1
13	12	mldual2i 1125	. . . . . 6 a0 a1 b1 a0 b0 b1 a0 a1 b1 a0 b0 b1
14		orcom 73	. . . . . . 7 a0 a1 b1 a0 b0 b1 a0 b0 b1 a0 a1 b1
15		ancom 74	. . . . . . . 8 a0 a1 b1 b1 a0 a1
16	15	lor 70	. . . . . . 7 a0 b0 b1 a0 a1 b1 a0 b0 b1 b1 a0 a1
17	14, 16	tr 62	. . . . . 6 a0 a1 b1 a0 b0 b1 a0 b0 b1 b1 a0 a1
18	11, 13, 17	3tr 65	. . . . 5 a0 a1 b0 b1 a0 b1 a0 b0 b1 b1 a0 a1
19	3, 4, 18	3tr 65	. . . 4 c2 a0 b1 a0 b0 b1 b1 a0 a1
20	19	lor 70	. . 3 c2 c0 c1 c2 a0 b1 c2 c0 c1 a0 b0 b1 b1 a0 a1
21	1, 20	tr 62	. 2 c2 c0 c1 c2 a0 b1 c2 c0 c1 a0 b0 b1 b1 a0 a1
22		lear 161	. . 3 c2 c0 c1 c0 c1
23	22	leror 152	. 2 c2 c0 c1 a0 b0 b1 b1 a0 a1 c0 c1 a0 b0 b1 b1 a0 a1
24	21, 23	bltr 138	1 c2 c0 c1 c2 a0 b1 c0 c1 a0 b0 b1 b1 a0 a1

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:  dp41lemm  1192

Copyright terms: Public domain

W3C validator