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

---

Theorem dp53lemb 1162

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

---

Proof of Theorem dp53lemb

Step	Hyp	Ref	Expression
1		dp53lem.3	. . . . . . 7 c2 a0 a1 b0 b1
2	1	ran 78	. . . . . 6 c2 c0 c1 a0 a1 b0 b1 c0 c1
3		an32 83	. . . . . 6 a0 a1 b0 b1 c0 c1 a0 a1 c0 c1 b0 b1
4	2, 3	tr 62	. . . . 5 c2 c0 c1 a0 a1 c0 c1 b0 b1
5	4	lor 70	. . . 4 b1 c2 c0 c1 b1 a0 a1 c0 c1 b0 b1
6		leor 159	. . . . 5 b1 b0 b1
7	6	ml2i 1123	. . . 4 b1 a0 a1 c0 c1 b0 b1 b1 a0 a1 c0 c1 b0 b1
8		ancom 74	. . . 4 b1 a0 a1 c0 c1 b0 b1 b0 b1 b1 a0 a1 c0 c1
9	5, 7, 8	3tr 65	. . 3 b1 c2 c0 c1 b0 b1 b1 a0 a1 c0 c1
10	9	lan 77	. 2 b0 b1 c2 c0 c1 b0 b0 b1 b1 a0 a1 c0 c1
11		anass 76	. . 3 b0 b0 b1 b1 a0 a1 c0 c1 b0 b0 b1 b1 a0 a1 c0 c1
12	11	cm 61	. 2 b0 b0 b1 b1 a0 a1 c0 c1 b0 b0 b1 b1 a0 a1 c0 c1
13		anabs 121	. . 3 b0 b0 b1 b0
14	13	ran 78	. 2 b0 b0 b1 b1 a0 a1 c0 c1 b0 b1 a0 a1 c0 c1
15	10, 12, 14	3tr 65	1 b0 b1 c2 c0 c1 b0 b1 a0 a1 c0 c1

Colors of variables: term

Syntax hints:   wb 1   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  ax-ml 1120

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:  dp53lemd  1164

Copyright terms: Public domain

W3C validator