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

---

Theorem dp53leme 1165

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

---

Proof of Theorem dp53leme

Step	Hyp	Ref	Expression
1		dp53lem.1	. . 3 c0 a1 a2 b1 b2
2		dp53lem.2	. . 3 c1 a0 a2 b0 b2
3		dp53lem.3	. . 3 c2 a0 a1 b0 b1
4		dp53lem.4	. . 3 p0 a1 b1 a2 b2
5		dp53lem.5	. . 3 a0 b0 a1 b1 a2 b2
6	1, 2, 3, 4, 5	dp53lemd 1164	. 2 b0 a0 p0 b0 a0 b0 b1 c2 c0 c1
7		orass 75	. . . . . 6 a0 b0 b1 c2 c0 c1 a0 b0 b1 c2 c0 c1
8		orcom 73	. . . . . 6 a0 b0 b1 c2 c0 c1 b1 c2 c0 c1 a0 b0
9	7, 8	tr 62	. . . . 5 a0 b0 b1 c2 c0 c1 b1 c2 c0 c1 a0 b0
10	9	lan 77	. . . 4 b0 a0 b0 b1 c2 c0 c1 b0 b1 c2 c0 c1 a0 b0
11		lear 161	. . . . 5 a0 b0 b0
12	11	mldual2i 1125	. . . 4 b0 b1 c2 c0 c1 a0 b0 b0 b1 c2 c0 c1 a0 b0
13		orcom 73	. . . 4 b0 b1 c2 c0 c1 a0 b0 a0 b0 b0 b1 c2 c0 c1
14	10, 12, 13	3tr 65	. . 3 b0 a0 b0 b1 c2 c0 c1 a0 b0 b0 b1 c2 c0 c1
15		lea 160	. . . 4 a0 b0 a0
16	15	leror 152	. . 3 a0 b0 b0 b1 c2 c0 c1 a0 b0 b1 c2 c0 c1
17	14, 16	bltr 138	. 2 b0 a0 b0 b1 c2 c0 c1 a0 b0 b1 c2 c0 c1
18	6, 17	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:  dp53lemf  1166

Copyright terms: Public domain

W3C validator