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

---

Theorem dp41lemm 1192

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
dp41lemm	c2 c0 c1

---

Proof of Theorem dp41lemm

Step	Hyp	Ref	Expression
1		dp41lem.1	. . . . . . . 8 c0 a1 a2 b1 b2
2		dp41lem.2	. . . . . . . 8 c1 a0 a2 b0 b2
3		dp41lem.3	. . . . . . . 8 c2 a0 a1 b0 b1
4		dp41lem.4	. . . . . . . 8 a0 b0 a1 b1 a2 b2
5		dp41lem.5	. . . . . . . 8 p2 a0 b0 a1 b1
6		dp41lem.6	. . . . . . . 8 p2 a2 b2
7	1, 2, 3, 4, 5, 6	dp41lemb 1181	. . . . . . 7 c2 c2 a0 b0 b1 a0 a1 b1
8	1, 2, 3, 4, 5, 6	dp41lemc 1183	. . . . . . 7 c2 a0 b0 b1 a0 a1 b1 c2 a0 b1 c2 c0 c1
9	7, 8	bltr 138	. . . . . 6 c2 c2 a0 b1 c2 c0 c1
10	1, 2, 3, 4, 5, 6	dp41lemd 1184	. . . . . 6 c2 a0 b1 c2 c0 c1 c2 c0 c1 c2 a0 b1
11	9, 10	lbtr 139	. . . . 5 c2 c2 c0 c1 c2 a0 b1
12	1, 2, 3, 4, 5, 6	dp41leme 1185	. . . . 5 c2 c0 c1 c2 a0 b1 c0 c1 a0 b0 b1 b1 a0 a1
13	11, 12	letr 137	. . . 4 c2 c0 c1 a0 b0 b1 b1 a0 a1
14	1, 2, 3, 4, 5, 6	dp41lemf 1186	. . . . 5 c0 c1 a0 b0 b1 b1 a0 a1 b1 b2 a1 a2 b1 a0 a1 a0 a2 b0 b2 a0 b0 b1
15	1, 2, 3, 4, 5, 6	dp41lemg 1187	. . . . 5 b1 b2 a1 a2 b1 a0 a1 a0 a2 b0 b2 a0 b0 b1 b1 b2 a1 a2 a0 a1 b1 a0 a2 b0 b2 b1 a0 b0
16	14, 15	tr 62	. . . 4 c0 c1 a0 b0 b1 b1 a0 a1 b1 b2 a1 a2 a0 a1 b1 a0 a2 b0 b2 b1 a0 b0
17	13, 16	lbtr 139	. . 3 c2 b1 b2 a1 a2 a0 a1 b1 a0 a2 b0 b2 b1 a0 b0
18	1, 2, 3, 4, 5, 6	dp41lemh 1188	. . 3 b1 b2 a1 a2 a0 a1 b1 a0 a2 b0 b2 b1 a0 b0 b1 b2 a1 a2 a0 a2 b2 a0 a2 b0 b2 b1 a2 b2
19	17, 18	letr 137	. 2 c2 b1 b2 a1 a2 a0 a2 b2 a0 a2 b0 b2 b1 a2 b2
20	1, 2, 3, 4, 5, 6	dp41lemj 1189	. . 3 b1 b2 a1 a2 a0 a2 b2 a0 a2 b0 b2 b1 a2 b2 b1 b2 a1 a2 b2 a0 a2 a0 a2 b0 b2 a2 b1 b2
21	1, 2, 3, 4, 5, 6	dp41lemk 1190	. . 3 b1 b2 a1 a2 b2 a0 a2 a0 a2 b0 b2 a2 b1 b2 c0 b2 a0 a2 c1 a2 b1 b2
22	1, 2, 3, 4, 5, 6	dp41leml 1191	. . 3 c0 b2 a0 a2 c1 a2 b1 b2 c0 c1
23	20, 21, 22	3tr 65	. 2 b1 b2 a1 a2 a0 a2 b2 a0 a2 b0 b2 b1 a2 b2 c0 c1
24	19, 23	lbtr 139	1 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:  dp41  1193

Copyright terms: Public domain

W3C validator