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

---

Theorem oa6fromdualn 954

Description: Dual to conventional 6-variable OA law.

Hypothesis

Ref	Expression
oa6fromdualn.1

Assertion

Ref	Expression
oa6fromdualn

---

Proof of Theorem oa6fromdualn

Step	Hyp	Ref	Expression
1		oa6fromdualn.1	. . 3
2		ax-a1 30	. . . 4
3		ax-a1 30	. . . . 5
4		ax-a1 30	. . . . . 6
5	3, 4	2an 79	. . . . . . . 8
6		ax-a1 30	. . . . . . . . 9
7	2, 6	2an 79	. . . . . . . 8
8	5, 7	2or 72	. . . . . . 7
9		ax-a1 30	. . . . . . . . . 10
10	3, 9	2an 79	. . . . . . . . 9
11		ax-a1 30	. . . . . . . . . 10
12	2, 11	2an 79	. . . . . . . . 9
13	10, 12	2or 72	. . . . . . . 8
14	4, 9	2an 79	. . . . . . . . 9
15	6, 11	2an 79	. . . . . . . . 9
16	14, 15	2or 72	. . . . . . . 8
17	13, 16	2an 79	. . . . . . 7
18	8, 17	2or 72	. . . . . 6
19	4, 18	2an 79	. . . . 5
20	3, 19	2or 72	. . . 4
21	2, 20	2an 79	. . 3
22	3, 2	2an 79	. . . . 5
23	4, 6	2an 79	. . . . 5
24	22, 23	2or 72	. . . 4
25	9, 11	2an 79	. . . 4
26	24, 25	2or 72	. . 3
27	1, 21, 26	le3tr2 141	. 2
28	27	oa6fromdual 953	1

Colors of variables: term

Syntax hints:   wle 2  wn 4   wo 6   wa 7

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

This theorem depends on definitions:  df-a 40  df-le1 130  df-le2 131

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator