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

---

Theorem oadp35lemc 1209

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

Hypotheses

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

Assertion

Ref	Expression
oadp35lemc	b0 a0 b0 b1 c2 c0 c1 b0 b1 c2 c0 c1

---

Proof of Theorem oadp35lemc

Step	Hyp	Ref	Expression
1		or32 82	. . 3 a0 b0 b1 c2 c0 c1 a0 b0 c2 c0 c1 b1
2		orcom 73	. . 3 a0 b0 c2 c0 c1 b1 b1 a0 b0 c2 c0 c1
3		leo 158	. . . . . . . 8 a0 a0 a1
4		leo 158	. . . . . . . 8 b0 b0 b1
5	3, 4	le2an 169	. . . . . . 7 a0 b0 a0 a1 b0 b1
6		oadp35lem.3	. . . . . . . 8 c2 a0 a1 b0 b1
7	6	cm 61	. . . . . . 7 a0 a1 b0 b1 c2
8	5, 7	lbtr 139	. . . . . 6 a0 b0 c2
9		leo 158	. . . . . . . . 9 a0 a0 a2
10		leo 158	. . . . . . . . 9 b0 b0 b2
11	9, 10	le2an 169	. . . . . . . 8 a0 b0 a0 a2 b0 b2
12		oadp35lem.2	. . . . . . . . 9 c1 a0 a2 b0 b2
13	12	cm 61	. . . . . . . 8 a0 a2 b0 b2 c1
14	11, 13	lbtr 139	. . . . . . 7 a0 b0 c1
15	14	lerr 150	. . . . . 6 a0 b0 c0 c1
16	8, 15	ler2an 173	. . . . 5 a0 b0 c2 c0 c1
17	16	df-le2 131	. . . 4 a0 b0 c2 c0 c1 c2 c0 c1
18	17	lor 70	. . 3 b1 a0 b0 c2 c0 c1 b1 c2 c0 c1
19	1, 2, 18	3tr 65	. 2 a0 b0 b1 c2 c0 c1 b1 c2 c0 c1
20	19	lan 77	1 b0 a0 b0 b1 c2 c0 c1 b0 b1 c2 c0 c1

Colors of variables: term

Syntax hints:   wb 1   wo 6   wa 7

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

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