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

---

Theorem dp34 1179

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). (3)=>(4)

Hypotheses

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

Assertion

Ref	Expression
dp34	a0 b1 c2 c0 c1

---

Proof of Theorem dp34

Step	Hyp	Ref	Expression
1		dp34.1	. . . 4 c0 a1 a2 b1 b2
2		dp34.2	. . . 4 c1 a0 a2 b0 b2
3		dp34.3	. . . 4 c2 a0 a1 b0 b1
4		dp34.4	. . . 4 a0 b0 a1 b1 a2 b2
5	1, 2, 3, 4	dp53 1168	. . 3 a0 b0 b1 c2 c0 c1
6		lear 161	. . . 4 b0 b1 c2 c0 c1 b1 c2 c0 c1
7	6	lelor 166	. . 3 a0 b0 b1 c2 c0 c1 a0 b1 c2 c0 c1
8	5, 7	letr 137	. 2 a0 b1 c2 c0 c1
9		orass 75	. . 3 a0 b1 c2 c0 c1 a0 b1 c2 c0 c1
10	9	cm 61	. 2 a0 b1 c2 c0 c1 a0 b1 c2 c0 c1
11	8, 10	lbtr 139	1 a0 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:  dp41lema  1180  xdp41  1196  xxdp41  1199  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206

Copyright terms: Public domain

W3C validator