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

---

Theorem dp41lemj 1189

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
dp41lemj	b1 b2 a1 a2 a0 a2 b2 a0 a2 b0 b2 b1 a2 b2 b1 b2 a1 a2 b2 a0 a2 a0 a2 b0 b2 a2 b1 b2

---

Proof of Theorem dp41lemj

Step	Hyp	Ref	Expression
1		ax-a2 31	. . . . . . . 8 a2 b2 b2 a2
2	1	lan 77	. . . . . . 7 a0 a2 b2 a0 b2 a2
3	2	lor 70	. . . . . 6 a2 a0 a2 b2 a2 a0 b2 a2
4		ml3 1128	. . . . . 6 a2 a0 b2 a2 a2 b2 a0 a2
5	3, 4	tr 62	. . . . 5 a2 a0 a2 b2 a2 b2 a0 a2
6	5	lor 70	. . . 4 a1 a2 a0 a2 b2 a1 a2 b2 a0 a2
7		orass 75	. . . 4 a1 a2 a0 a2 b2 a1 a2 a0 a2 b2
8		orass 75	. . . 4 a1 a2 b2 a0 a2 a1 a2 b2 a0 a2
9	6, 7, 8	3tr1 63	. . 3 a1 a2 a0 a2 b2 a1 a2 b2 a0 a2
10	9	lan 77	. 2 b1 b2 a1 a2 a0 a2 b2 b1 b2 a1 a2 b2 a0 a2
11		ml3 1128	. . . . 5 b2 b1 a2 b2 b2 a2 b1 b2
12	11	lor 70	. . . 4 b0 b2 b1 a2 b2 b0 b2 a2 b1 b2
13		orass 75	. . . 4 b0 b2 b1 a2 b2 b0 b2 b1 a2 b2
14		orass 75	. . . 4 b0 b2 a2 b1 b2 b0 b2 a2 b1 b2
15	12, 13, 14	3tr1 63	. . 3 b0 b2 b1 a2 b2 b0 b2 a2 b1 b2
16	15	lan 77	. 2 a0 a2 b0 b2 b1 a2 b2 a0 a2 b0 b2 a2 b1 b2
17	10, 16	2or 72	1 b1 b2 a1 a2 a0 a2 b2 a0 a2 b0 b2 b1 a2 b2 b1 b2 a1 a2 b2 a0 a2 a0 a2 b0 b2 a2 b1 b2

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

Copyright terms: Public domain

W3C validator