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

---

Theorem dp15lemc 1154

Description: Part of proof (1)=>(5) in Day/Pickering 1982.

Hypotheses

Ref	Expression
dp15lema.1	a2 a0 a1 b1
dp15lema.2	p0 a1 b1 a2 b2
dp15lema.3	b0 a0 p0

Assertion

Ref	Expression
dp15lemc	a0 a1 b0 a0 p0 b1 a0 a2 a0 a1 b1 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2

---

Proof of Theorem dp15lemc

Step	Hyp	Ref	Expression
1		dp15lema.1	. . 3 a2 a0 a1 b1
2		dp15lema.2	. . 3 p0 a1 b1 a2 b2
3		dp15lema.3	. . 3 b0 a0 p0
4	1, 2, 3	dp15lemb 1153	. 2 a0 a1 b1 a0 b2 a1 b1 b2
5	3	ror 71	. . 3 b1 b0 a0 p0 b1
6	5	lan 77	. 2 a0 a1 b1 a0 a1 b0 a0 p0 b1
7	1	lor 70	. . . 4 a0 a0 a2 a0 a1 b1
8	3	ror 71	. . . 4 b2 b0 a0 p0 b2
9	7, 8	2an 79	. . 3 a0 b2 a0 a2 a0 a1 b1 b0 a0 p0 b2
10	1	lor 70	. . . 4 a1 a1 a2 a0 a1 b1
11	10	ran 78	. . 3 a1 b1 b2 a1 a2 a0 a1 b1 b1 b2
12	9, 11	2or 72	. 2 a0 b2 a1 b1 b2 a0 a2 a0 a1 b1 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2
13	4, 6, 12	le3tr2 141	1 a0 a1 b0 a0 p0 b1 a0 a2 a0 a1 b1 b0 a0 p0 b2 a1 a2 a0 a1 b1 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-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:  dp15lemh  1159

Copyright terms: Public domain

W3C validator