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

---

Theorem dp35lemd 1172

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
dp35lemd	b0 a0 p0 b0 a0 b0 b1 c2 c0 c1

---

Proof of Theorem dp35lemd

Step	Hyp	Ref	Expression
1		lea 160	. . 3 b0 a0 p0 b0
2		dp35lem.1	. . . 4 c0 a1 a2 b1 b2
3		dp35lem.2	. . . 4 c1 a0 a2 b0 b2
4		dp35lem.3	. . . 4 c2 a0 a1 b0 b1
5		dp35lem.4	. . . 4 p0 a1 b1 a2 b2
6		dp35lem.5	. . . 4 a0 b0 a1 b1 a2 b2
7	2, 3, 4, 5, 6	dp35leme 1171	. . 3 b0 a0 p0 a0 b0 b1 c2 c0 c1
8	1, 7	ler2an 173	. 2 b0 a0 p0 b0 a0 b0 b1 c2 c0 c1
9		lea 160	. . . 4 b0 b1 c2 c0 c1 b0
10	9	mldual2i 1125	. . 3 b0 a0 b0 b1 c2 c0 c1 b0 a0 b0 b1 c2 c0 c1
11		lea 160	. . . . 5 b0 a0 b0
12	11, 9	lel2or 170	. . . 4 b0 a0 b0 b1 c2 c0 c1 b0
13		ancom 74	. . . . . . 7 b0 a0 a0 b0
14	13	bile 142	. . . . . 6 b0 a0 a0 b0
15		lear 161	. . . . . 6 b0 b1 c2 c0 c1 b1 c2 c0 c1
16	14, 15	le2or 168	. . . . 5 b0 a0 b0 b1 c2 c0 c1 a0 b0 b1 c2 c0 c1
17		orass 75	. . . . . 6 a0 b0 b1 c2 c0 c1 a0 b0 b1 c2 c0 c1
18	17	cm 61	. . . . 5 a0 b0 b1 c2 c0 c1 a0 b0 b1 c2 c0 c1
19	16, 18	lbtr 139	. . . 4 b0 a0 b0 b1 c2 c0 c1 a0 b0 b1 c2 c0 c1
20	12, 19	ler2an 173	. . 3 b0 a0 b0 b1 c2 c0 c1 b0 a0 b0 b1 c2 c0 c1
21	10, 20	bltr 138	. 2 b0 a0 b0 b1 c2 c0 c1 b0 a0 b0 b1 c2 c0 c1
22	8, 21	letr 137	1 b0 a0 p0 b0 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:  dp35lembb  1175

Copyright terms: Public domain

W3C validator