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

---

Theorem oadp35lemf 1208

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
oadp35lemf	a0 a0 b0 b1 c2 c0 c1

---

Proof of Theorem oadp35lemf

Step	Hyp	Ref	Expression
1		leo 158	. 2 a0 a0 b0 b1 c2 c0 c1
2		oadp35lem.1	. . 3 c0 a1 a2 b1 b2
3		oadp35lem.2	. . 3 c1 a0 a2 b0 b2
4		oadp35lem.3	. . 3 c2 a0 a1 b0 b1
5		oadp35lem.4	. . 3 p0 a1 b1 a2 b2
6		oadp35lem.5	. . 3 a0 b0 a1 b1 a2 b2
7	2, 3, 4, 5, 6	oadp35lemg 1207	. 2 a0 b0 b1 c2 c0 c1
8	1, 7	lel2or 170	1 a0 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