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

---

Theorem dp53lemf 1166

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

Hypotheses

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

Assertion

Ref	Expression
dp53lemf	a0 a0 b0 b1 c2 c0 c1

---

Proof of Theorem dp53lemf

Step	Hyp	Ref	Expression
1		leo 158	. 2 a0 a0 b0 b1 c2 c0 c1
2		dp53lem.5	. . . . . . 7 a0 b0 a1 b1 a2 b2
3		anass 76	. . . . . . 7 a0 b0 a1 b1 a2 b2 a0 b0 a1 b1 a2 b2
4	2, 3	tr 62	. . . . . 6 a0 b0 a1 b1 a2 b2
5		dp53lem.4	. . . . . . . . . 10 p0 a1 b1 a2 b2
6	5	lan 77	. . . . . . . . 9 a0 b0 p0 a0 b0 a1 b1 a2 b2
7	6	cm 61	. . . . . . . 8 a0 b0 a1 b1 a2 b2 a0 b0 p0
8		leao4 165	. . . . . . . 8 a0 b0 p0 a0 p0
9	7, 8	bltr 138	. . . . . . 7 a0 b0 a1 b1 a2 b2 a0 p0
10		lea 160	. . . . . . . 8 a0 b0 a1 b1 a2 b2 a0 b0
11		orcom 73	. . . . . . . 8 a0 b0 b0 a0
12	10, 11	lbtr 139	. . . . . . 7 a0 b0 a1 b1 a2 b2 b0 a0
13	9, 12	ler2an 173	. . . . . 6 a0 b0 a1 b1 a2 b2 a0 p0 b0 a0
14	4, 13	bltr 138	. . . . 5 a0 p0 b0 a0
15		leo 158	. . . . . . 7 a0 a0 p0
16	15	mldual2i 1125	. . . . . 6 a0 p0 b0 a0 a0 p0 b0 a0
17		ancom 74	. . . . . . 7 a0 p0 b0 b0 a0 p0
18	17	ror 71	. . . . . 6 a0 p0 b0 a0 b0 a0 p0 a0
19	16, 18	tr 62	. . . . 5 a0 p0 b0 a0 b0 a0 p0 a0
20	14, 19	lbtr 139	. . . 4 b0 a0 p0 a0
21	1	lelor 166	. . . 4 b0 a0 p0 a0 b0 a0 p0 a0 b0 b1 c2 c0 c1
22	20, 21	letr 137	. . 3 b0 a0 p0 a0 b0 b1 c2 c0 c1
23		dp53lem.1	. . . . 5 c0 a1 a2 b1 b2
24		dp53lem.2	. . . . 5 c1 a0 a2 b0 b2
25		dp53lem.3	. . . . 5 c2 a0 a1 b0 b1
26	23, 24, 25, 5, 2	dp53leme 1165	. . . 4 b0 a0 p0 a0 b0 b1 c2 c0 c1
27	26	df-le2 131	. . 3 b0 a0 p0 a0 b0 b1 c2 c0 c1 a0 b0 b1 c2 c0 c1
28	22, 27	lbtr 139	. 2 a0 b0 b1 c2 c0 c1
29	1, 28	lel2or 170	1 a0 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:  dp53lemg  1167

Copyright terms: Public domain

W3C validator