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

---

Theorem dp41leml 1191

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
dp41leml	c0 b2 a0 a2 c1 a2 b1 b2 c0 c1

---

Proof of Theorem dp41leml

Step	Hyp	Ref	Expression
1		or4 84	. 2 c0 b2 a0 a2 c1 a2 b1 b2 c0 c1 b2 a0 a2 a2 b1 b2
2		orcom 73	. 2 c0 c1 b2 a0 a2 a2 b1 b2 b2 a0 a2 a2 b1 b2 c0 c1
3		ancom 74	. . . . . 6 b2 a0 a2 a0 a2 b2
4		leor 159	. . . . . . 7 b2 b0 b2
5	4	lelan 167	. . . . . 6 a0 a2 b2 a0 a2 b0 b2
6	3, 5	bltr 138	. . . . 5 b2 a0 a2 a0 a2 b0 b2
7		leor 159	. . . . . 6 a2 a1 a2
8	7	leran 153	. . . . 5 a2 b1 b2 a1 a2 b1 b2
9	6, 8	le2or 168	. . . 4 b2 a0 a2 a2 b1 b2 a0 a2 b0 b2 a1 a2 b1 b2
10		dp41lem.2	. . . . . . 7 c1 a0 a2 b0 b2
11		dp41lem.1	. . . . . . 7 c0 a1 a2 b1 b2
12	10, 11	2or 72	. . . . . 6 c1 c0 a0 a2 b0 b2 a1 a2 b1 b2
13	12	cm 61	. . . . 5 a0 a2 b0 b2 a1 a2 b1 b2 c1 c0
14		orcom 73	. . . . 5 c1 c0 c0 c1
15	13, 14	tr 62	. . . 4 a0 a2 b0 b2 a1 a2 b1 b2 c0 c1
16	9, 15	lbtr 139	. . 3 b2 a0 a2 a2 b1 b2 c0 c1
17	16	df-le2 131	. 2 b2 a0 a2 a2 b1 b2 c0 c1 c0 c1
18	1, 2, 17	3tr 65	1 c0 b2 a0 a2 c1 a2 b1 b2 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-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

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:  dp41lemm  1192

Copyright terms: Public domain

W3C validator