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

---

Theorem dp35lembb 1175

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

Hypotheses

Ref	Expression
dp35lem.1	c0 a1 a2 b1 b2
dp35lem.2	c1 a0 a2 b0 b2
dp35lem.3	c2 a0 a1 b0 b1
dp35lem.4	p0 a1 b1 a2 b2
dp35lem.5	a0 b0 a1 b1 a2 b2

Assertion

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

---

Proof of Theorem dp35lembb

Step	Hyp	Ref	Expression
1		dp35lem.1	. . 3 c0 a1 a2 b1 b2
2		dp35lem.2	. . 3 c1 a0 a2 b0 b2
3		dp35lem.3	. . 3 c2 a0 a1 b0 b1
4		dp35lem.4	. . 3 p0 a1 b1 a2 b2
5		dp35lem.5	. . 3 a0 b0 a1 b1 a2 b2
6	1, 2, 3, 4, 5	dp35lemd 1172	. 2 b0 a0 p0 b0 a0 b0 b1 c2 c0 c1
7	1, 2, 3, 4, 5	dp35lemc 1173	. . 3 b0 a0 b0 b1 c2 c0 c1 b0 b1 c2 c0 c1
8	1, 2, 3, 4, 5	dp35lemb 1174	. . 3 b0 b1 c2 c0 c1 b0 b1 a0 a1 c0 c1
9	7, 8	tr 62	. 2 b0 a0 b0 b1 c2 c0 c1 b0 b1 a0 a1 c0 c1
10	6, 9	lbtr 139	1 b0 a0 p0 b0 b1 a0 a1 c0 c1

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:  dp35lema  1176

Copyright terms: Public domain

W3C validator