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

---

Theorem dp41lemf 1186

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
dp41lemf	c0 c1 a0 b0 b1 b1 a0 a1 b1 b2 a1 a2 b1 a0 a1 a0 a2 b0 b2 a0 b0 b1

---

Proof of Theorem dp41lemf

Step	Hyp	Ref	Expression
1		orcom 73	. . 3 a0 b0 b1 b1 a0 a1 b1 a0 a1 a0 b0 b1
2	1	lor 70	. 2 c0 c1 a0 b0 b1 b1 a0 a1 c0 c1 b1 a0 a1 a0 b0 b1
3		or4 84	. . 3 c0 c1 b1 a0 a1 a0 b0 b1 c0 b1 a0 a1 c1 a0 b0 b1
4		dp41lem.1	. . . . . 6 c0 a1 a2 b1 b2
5		ancom 74	. . . . . 6 a1 a2 b1 b2 b1 b2 a1 a2
6	4, 5	tr 62	. . . . 5 c0 b1 b2 a1 a2
7	6	ror 71	. . . 4 c0 b1 a0 a1 b1 b2 a1 a2 b1 a0 a1
8		dp41lem.2	. . . . 5 c1 a0 a2 b0 b2
9	8	ror 71	. . . 4 c1 a0 b0 b1 a0 a2 b0 b2 a0 b0 b1
10	7, 9	2or 72	. . 3 c0 b1 a0 a1 c1 a0 b0 b1 b1 b2 a1 a2 b1 a0 a1 a0 a2 b0 b2 a0 b0 b1
11	3, 10	tr 62	. 2 c0 c1 b1 a0 a1 a0 b0 b1 b1 b2 a1 a2 b1 a0 a1 a0 a2 b0 b2 a0 b0 b1
12		leao1 162	. . . 4 b1 a0 a1 b1 b2
13	12	mli 1124	. . 3 b1 b2 a1 a2 b1 a0 a1 b1 b2 a1 a2 b1 a0 a1
14		leao1 162	. . . 4 a0 b0 b1 a0 a2
15	14	mli 1124	. . 3 a0 a2 b0 b2 a0 b0 b1 a0 a2 b0 b2 a0 b0 b1
16	13, 15	2or 72	. 2 b1 b2 a1 a2 b1 a0 a1 a0 a2 b0 b2 a0 b0 b1 b1 b2 a1 a2 b1 a0 a1 a0 a2 b0 b2 a0 b0 b1
17	2, 11, 16	3tr 65	1 c0 c1 a0 b0 b1 b1 a0 a1 b1 b2 a1 a2 b1 a0 a1 a0 a2 b0 b2 a0 b0 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  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