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

---

Theorem dp23 1195

Description: Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (2)=>(3)

Hypotheses

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

Assertion

Ref	Expression
dp23	a0 b0 b1 c2 c0 c1

---

Proof of Theorem dp23

Step	Hyp	Ref	Expression
1		dp23.1	. . 3 c0 a1 a2 b1 b2
2		dp23.2	. . 3 c1 a0 a2 b0 b2
3		dp23.3	. . 3 c2 a0 a1 b0 b1
4		dp23.4	. . 3 a0 b0 a1 b1 a2 b2
5	1, 2, 3, 4	dp32 1194	. 2 a0 a1 c2 c0 c1 b0 b1 c2 c0 c1
6		lea 160	. . 3 a0 a1 c2 c0 c1 a0
7	6	leror 152	. 2 a0 a1 c2 c0 c1 b0 b1 c2 c0 c1 a0 b0 b1 c2 c0 c1
8	5, 7	letr 137	1 a0 b0 b1 c2 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: (None)

Copyright terms: Public domain

W3C validator