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

---

Theorem dp15lemg 1158

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

Hypotheses

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

Assertion

Ref	Expression
dp15lemg	a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1 c0 c1 b1 a0 a1

---

Proof of Theorem dp15lemg

Step	Hyp	Ref	Expression
1		dp15lemg.4	. . . 4 c0 a1 a2 b1 b2
2		dp15lemg.5	. . . . 5 c1 a0 a2 b0 b2
3	2	ror 71	. . . 4 c1 b1 a0 a1 a0 a2 b0 b2 b1 a0 a1
4	1, 3	2or 72	. . 3 c0 c1 b1 a0 a1 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1
5	4	cm 61	. 2 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1 c0 c1 b1 a0 a1
6		orass 75	. . 3 c0 c1 b1 a0 a1 c0 c1 b1 a0 a1
7	6	cm 61	. 2 c0 c1 b1 a0 a1 c0 c1 b1 a0 a1
8	5, 7	tr 62	1 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1 c0 c1 b1 a0 a1

Colors of variables: term

Syntax hints:   wb 1   wo 6   wa 7

This theorem was proved from axioms:  ax-a2 31  ax-a3 32  ax-r1 35  ax-r2 36  ax-r5 38

This theorem is referenced by:  dp15lemh  1159

Copyright terms: Public domain

W3C validator