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

---

Theorem dp15lemh 1159

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
dp15lemg.4	c0 a1 a2 b1 b2
dp15lemg.5	c1 a0 a2 b0 b2

Assertion

Ref	Expression
dp15lemh	a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1

---

Proof of Theorem dp15lemh

Step	Hyp	Ref	Expression
1		dp15lema.1	. . . . . 6 a2 a0 a1 b1
2		dp15lema.2	. . . . . 6 p0 a1 b1 a2 b2
3		dp15lema.3	. . . . . 6 b0 a0 p0
4	1, 2, 3	dp15lemc 1154	. . . . 5 a0 a1 b0 a0 p0 b1 a0 a2 a0 a1 b1 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2
5	1, 2, 3	dp15lemd 1155	. . . . 5 a0 a2 a0 a1 b1 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2 a0 a2 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2
6	4, 5	lbtr 139	. . . 4 a0 a1 b0 a0 p0 b1 a0 a2 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2
7	1, 2, 3	dp15leme 1156	. . . 4 a0 a2 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2 a0 a2 b0 a0 p0 b2 a1 a2 b1 a0 a1 b1 b2
8	6, 7	letr 137	. . 3 a0 a1 b0 a0 p0 b1 a0 a2 b0 a0 p0 b2 a1 a2 b1 a0 a1 b1 b2
9	1, 2, 3	dp15lemf 1157	. . 3 a0 a2 b0 a0 p0 b2 a1 a2 b1 a0 a1 b1 b2 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1
10	8, 9	letr 137	. 2 a0 a1 b0 a0 p0 b1 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1
11		dp15lemg.4	. . 3 c0 a1 a2 b1 b2
12		dp15lemg.5	. . 3 c1 a0 a2 b0 b2
13	1, 2, 3, 11, 12	dp15lemg 1158	. 2 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1 c0 c1 b1 a0 a1
14	10, 13	lbtr 139	1 a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1

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:  dp15  1160

Copyright terms: Public domain

W3C validator