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

---

Theorem dp35lem0 1177

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
dp35lem0	a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1

---

Proof of Theorem dp35lem0

Step	Hyp	Ref	Expression
1		orcom 73	. . . . . 6 b0 a0 p0 b1 b1 b0 a0 p0
2		leid 148	. . . . . 6 b1 b0 a0 p0 b1 b0 a0 p0
3	1, 2	bltr 138	. . . . 5 b0 a0 p0 b1 b1 b0 a0 p0
4		dp35lem.1	. . . . . 6 c0 a1 a2 b1 b2
5		dp35lem.2	. . . . . 6 c1 a0 a2 b0 b2
6		dp35lem.3	. . . . . 6 c2 a0 a1 b0 b1
7		dp35lem.4	. . . . . 6 p0 a1 b1 a2 b2
8		dp35lem.5	. . . . . 6 a0 b0 a1 b1 a2 b2
9	4, 5, 6, 7, 8	dp35lema 1176	. . . . 5 b1 b0 a0 p0 b1 a0 a1 c0 c1
10	3, 9	letr 137	. . . 4 b0 a0 p0 b1 b1 a0 a1 c0 c1
11	10	lelan 167	. . 3 a0 a1 b0 a0 p0 b1 a0 a1 b1 a0 a1 c0 c1
12		id 59	. . . . 5 a0 a1 b1 a0 a1 c0 c1 a0 a1 b1 a0 a1 c0 c1
13		lea 160	. . . . . 6 a0 a1 c0 c1 a0 a1
14	13	mldual2i 1125	. . . . 5 a0 a1 b1 a0 a1 c0 c1 a0 a1 b1 a0 a1 c0 c1
15	12, 14	tr 62	. . . 4 a0 a1 b1 a0 a1 c0 c1 a0 a1 b1 a0 a1 c0 c1
16		ancom 74	. . . . 5 a0 a1 b1 b1 a0 a1
17	16	ror 71	. . . 4 a0 a1 b1 a0 a1 c0 c1 b1 a0 a1 a0 a1 c0 c1
18	15, 17	tr 62	. . 3 a0 a1 b1 a0 a1 c0 c1 b1 a0 a1 a0 a1 c0 c1
19	11, 18	lbtr 139	. 2 a0 a1 b0 a0 p0 b1 b1 a0 a1 a0 a1 c0 c1
20		lear 161	. . . 4 a0 a1 c0 c1 c0 c1
21	20	lelor 166	. . 3 b1 a0 a1 a0 a1 c0 c1 b1 a0 a1 c0 c1
22		orcom 73	. . 3 b1 a0 a1 c0 c1 c0 c1 b1 a0 a1
23	21, 22	lbtr 139	. 2 b1 a0 a1 a0 a1 c0 c1 c0 c1 b1 a0 a1
24	19, 23	letr 137	1 a0 a1 b0 a0 p0 b1 c0 c1 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-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:  dp35  1178  oadp35  1210

Copyright terms: Public domain

W3C validator