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

---

Theorem dp15lemd 1155

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

Assertion

Ref	Expression
dp15lemd	a0 a2 a0 a1 b1 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2 a0 a2 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2

---

Proof of Theorem dp15lemd

Step	Hyp	Ref	Expression
1		or12 80	. . . 4 a0 a2 a0 a1 b1 a2 a0 a0 a1 b1
2		orabs 120	. . . . 5 a0 a0 a1 b1 a0
3	2	lor 70	. . . 4 a2 a0 a0 a1 b1 a2 a0
4		orcom 73	. . . 4 a2 a0 a0 a2
5	1, 3, 4	3tr 65	. . 3 a0 a2 a0 a1 b1 a0 a2
6	5	ran 78	. 2 a0 a2 a0 a1 b1 b0 a0 p0 b2 a0 a2 b0 a0 p0 b2
7		orass 75	. . . 4 a1 a2 a0 a1 b1 a1 a2 a0 a1 b1
8	7	ran 78	. . 3 a1 a2 a0 a1 b1 b1 b2 a1 a2 a0 a1 b1 b1 b2
9	8	cm 61	. 2 a1 a2 a0 a1 b1 b1 b2 a1 a2 a0 a1 b1 b1 b2
10	6, 9	2or 72	1 a0 a2 a0 a1 b1 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2 a0 a2 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2

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-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-a 40

This theorem is referenced by:  dp15lemh  1159

Copyright terms: Public domain

W3C validator