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

---

Theorem oa3moa3 1029

Description: 4-variable 3OA to 5-variable Mayet's 3OA.

Hypotheses

Ref	Expression
oa3moa3.1
oa3moa3.2
oa3moa3.3
oa3moa3.4

Assertion

Ref	Expression
oa3moa3

---

Proof of Theorem oa3moa3

Step	Hyp	Ref	Expression
1		oa3moa3.1	. . . . . 6
2	1	lecon3 157	. . . . 5
3		oa3moa3.2	. . . . . . . 8
4	3	lecon3 157	. . . . . . 7
5		oa3moa3.4	. . . . . . 7
6	4, 5	lel2or 170	. . . . . 6
7	6	lecon3 157	. . . . 5
8	2, 7	ax-oal4 1026	. . . 4
9		ax-a2 31	. . . . 5
10		ax-a3 32	. . . . 5
11	9, 10	2an 79	. . . 4
12		orass 75	. . . . . . . 8
13	12	lan 77	. . . . . . 7
14	13	lor 70	. . . . . 6
15	14	lan 77	. . . . 5
16	15	lor 70	. . . 4
17	8, 11, 16	le3tr1 140	. . 3
18		oa3moa3.3	. . . . . . . . . 10
19	18	lecon3 157	. . . . . . . . 9
20	3, 19	lel2or 170	. . . . . . . 8
21	20	lecon3 157	. . . . . . 7
22	2, 21	ax-oal4 1026	. . . . . 6
23		ax-a2 31	. . . . . . . . 9
24	23	ror 71	. . . . . . . 8
25		orass 75	. . . . . . . 8
26	24, 25	tr 62	. . . . . . 7
27	9, 26	2an 79	. . . . . 6
28		orass 75	. . . . . . . . . 10
29	28	lan 77	. . . . . . . . 9
30	29	lor 70	. . . . . . . 8
31	30	lan 77	. . . . . . 7
32	31	lor 70	. . . . . 6
33	22, 27, 32	le3tr1 140	. . . . 5
34	5	lecon3 157	. . . . . . . . 9
35	34, 18	lel2or 170	. . . . . . . 8
36	35	lecon3 157	. . . . . . 7
37	2, 36	ax-oal4 1026	. . . . . 6
38		ax-a2 31	. . . . . . 7
39	9, 38	2an 79	. . . . . 6
40		ax-a3 32	. . . . . . . . . 10
41	40	lan 77	. . . . . . . . 9
42	41	lor 70	. . . . . . . 8
43	42	lan 77	. . . . . . 7
44	43	lor 70	. . . . . 6
45	37, 39, 44	le3tr1 140	. . . . 5
46	33, 45	ler2an 173	. . . 4
47	2	lel 151	. . . . . . . . . 10
48	47	lecom 180	. . . . . . . . 9
49	48	comcom7 460	. . . . . . . 8
50	49	comcom 453	. . . . . . 7
51	2	lel 151	. . . . . . . . . 10
52	51	lecom 180	. . . . . . . . 9
53	52	comcom7 460	. . . . . . . 8
54	53	comcom 453	. . . . . . 7
55	50, 54	fh3 471	. . . . . 6
56	55	cm 61	. . . . 5
57		anandi 114	. . . . . . 7
58	57	cm 61	. . . . . 6
59	58	lor 70	. . . . 5
60	56, 59	tr 62	. . . 4
61	46, 60	lbtr 139	. . 3
62	17, 61	ler2an 173	. 2
63	2	lel 151	. . . . . . . 8
64	63	lecom 180	. . . . . . 7
65	64	comcom7 460	. . . . . 6
66	65	comcom 453	. . . . 5
67	2	lel 151	. . . . . . . 8
68	67	lecom 180	. . . . . . 7
69	68	comcom7 460	. . . . . 6
70	69	comcom 453	. . . . 5
71	66, 70	fh3 471	. . . 4
72	71	ax-r1 35	. . 3
73		anass 76	. . . . . 6
74	73	cm 61	. . . . 5
75		anandi 114	. . . . . 6
76	75	ax-r1 35	. . . . 5
77		anass 76	. . . . 5
78	74, 76, 77	3tr1 63	. . . 4
79	78	lor 70	. . 3
80	72, 79	tr 62	. 2
81	62, 80	lbtr 139	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-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439  ax-oal4 1026

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator