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

---

Theorem dp41lemc 1183

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
dp41lemc	c2 a0 b0 b1 a0 a1 b1 c2 a0 b1 c2 c0 c1

---

Proof of Theorem dp41lemc

Step	Hyp	Ref	Expression
1		anass 76	. 2 c2 a0 b0 b1 a0 a1 b1 c2 a0 b0 b1 a0 a1 b1
2		dp41lem.1	. . . . 5 c0 a1 a2 b1 b2
3		dp41lem.2	. . . . 5 c1 a0 a2 b0 b2
4		dp41lem.3	. . . . 5 c2 a0 a1 b0 b1
5		dp41lem.4	. . . . 5 a0 b0 a1 b1 a2 b2
6		dp41lem.5	. . . . 5 p2 a0 b0 a1 b1
7		dp41lem.6	. . . . 5 p2 a2 b2
8	2, 3, 4, 5, 6, 7	dp41lemc0 1182	. . . 4 a0 b0 b1 a0 a1 b1 a0 b1 a0 b0 a1 b1
9		leo 158	. . . . 5 a0 b1 a0 b1 c2 c0 c1
10	2, 3, 4, 5, 6, 7	dp41lema 1180	. . . . 5 a0 b0 a1 b1 a0 b1 c2 c0 c1
11	9, 10	lel2or 170	. . . 4 a0 b1 a0 b0 a1 b1 a0 b1 c2 c0 c1
12	8, 11	bltr 138	. . 3 a0 b0 b1 a0 a1 b1 a0 b1 c2 c0 c1
13	12	lelan 167	. 2 c2 a0 b0 b1 a0 a1 b1 c2 a0 b1 c2 c0 c1
14	1, 13	bltr 138	1 c2 a0 b0 b1 a0 a1 b1 c2 a0 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:  dp41lemm  1192

Copyright terms: Public domain

W3C validator