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

---

Theorem dp41lemb 1181

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
dp41lemb	c2 c2 a0 b0 b1 a0 a1 b1

---

Proof of Theorem dp41lemb

Step	Hyp	Ref	Expression
1		dp41lem.3	. . . . . 6 c2 a0 a1 b0 b1
2		ancom 74	. . . . . 6 a0 a1 b0 b1 b0 b1 a0 a1
3	1, 2	tr 62	. . . . 5 c2 b0 b1 a0 a1
4		leor 159	. . . . . . 7 b0 a0 b0
5	4	leror 152	. . . . . 6 b0 b1 a0 b0 b1
6		leo 158	. . . . . 6 a0 a1 a0 a1 b1
7	5, 6	le2an 169	. . . . 5 b0 b1 a0 a1 a0 b0 b1 a0 a1 b1
8	3, 7	bltr 138	. . . 4 c2 a0 b0 b1 a0 a1 b1
9	8	df2le2 136	. . 3 c2 a0 b0 b1 a0 a1 b1 c2
10	9	cm 61	. 2 c2 c2 a0 b0 b1 a0 a1 b1
11		anass 76	. . 3 c2 a0 b0 b1 a0 a1 b1 c2 a0 b0 b1 a0 a1 b1
12	11	cm 61	. 2 c2 a0 b0 b1 a0 a1 b1 c2 a0 b0 b1 a0 a1 b1
13	10, 12	tr 62	1 c2 c2 a0 b0 b1 a0 a1 b1

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