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

---

Theorem dp35leme 1171

Description: Part of proof (3)=>(5) in Day/Pickering 1982.

Hypotheses

Ref	Expression
dp35lem.1	c0 a1 a2 b1 b2
dp35lem.2	c1 a0 a2 b0 b2
dp35lem.3	c2 a0 a1 b0 b1
dp35lem.4	p0 a1 b1 a2 b2
dp35lem.5	a0 b0 a1 b1 a2 b2

Assertion

Ref	Expression
dp35leme	b0 a0 p0 a0 b0 b1 c2 c0 c1

---

Proof of Theorem dp35leme

Step	Hyp	Ref	Expression
1		leor 159	. . 3 b0 a0 b0
2		dp35lem.4	. . . . 5 p0 a1 b1 a2 b2
3	2	lor 70	. . . 4 a0 p0 a0 a1 b1 a2 b2
4	3	bile 142	. . 3 a0 p0 a0 a1 b1 a2 b2
5	1, 4	le2an 169	. 2 b0 a0 p0 a0 b0 a0 a1 b1 a2 b2
6		ancom 74	. . . . . 6 a1 b1 a2 b2 a0 b0 a0 b0 a1 b1 a2 b2
7		anass 76	. . . . . . 7 a0 b0 a1 b1 a2 b2 a0 b0 a1 b1 a2 b2
8	7	cm 61	. . . . . 6 a0 b0 a1 b1 a2 b2 a0 b0 a1 b1 a2 b2
9	6, 8	tr 62	. . . . 5 a1 b1 a2 b2 a0 b0 a0 b0 a1 b1 a2 b2
10	9	lor 70	. . . 4 a0 a1 b1 a2 b2 a0 b0 a0 a0 b0 a1 b1 a2 b2
11		ancom 74	. . . . 5 a0 b0 a0 a1 b1 a2 b2 a0 a1 b1 a2 b2 a0 b0
12		leo 158	. . . . . 6 a0 a0 b0
13	12	mlduali 1126	. . . . 5 a0 a1 b1 a2 b2 a0 b0 a0 a1 b1 a2 b2 a0 b0
14	11, 13	tr 62	. . . 4 a0 b0 a0 a1 b1 a2 b2 a0 a1 b1 a2 b2 a0 b0
15		dp35lem.5	. . . . 5 a0 b0 a1 b1 a2 b2
16	15	lor 70	. . . 4 a0 a0 a0 b0 a1 b1 a2 b2
17	10, 14, 16	3tr1 63	. . 3 a0 b0 a0 a1 b1 a2 b2 a0
18		dp35lem.1	. . . 4 c0 a1 a2 b1 b2
19		dp35lem.2	. . . 4 c1 a0 a2 b0 b2
20		dp35lem.3	. . . 4 c2 a0 a1 b0 b1
21	18, 19, 20, 2, 15	dp35lemf 1170	. . 3 a0 a0 b0 b1 c2 c0 c1
22	17, 21	bltr 138	. 2 a0 b0 a0 a1 b1 a2 b2 a0 b0 b1 c2 c0 c1
23	5, 22	letr 137	1 b0 a0 p0 a0 b0 b1 c2 c0 c1

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-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-ml 1120  ax-arg 1151

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:  dp35lemd  1172

Copyright terms: Public domain

W3C validator