Quantum Logic Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa3-2to2s		Unicode version

---

Theorem oa3-2to2s 990

Description: Derivation of 3-OA variant from weaker version.

Hypotheses

Ref	Expression
oa3-2to2s.1
oa3-2to2s.2

Assertion

Ref	Expression
oa3-2to2s

---

Proof of Theorem oa3-2to2s

Step	Hyp	Ref	Expression
1		id 59	. . 3
2		id 59	. . 3
3		id 59	. . 3
4		leo 158	. . . . 5
5		df-i1 44	. . . . . . 7
6	5	ax-r1 35	. . . . . 6
7		ax-a1 30	. . . . . 6
8	6, 7	ax-r2 36	. . . . 5
9	4, 8	lbtr 139	. . . 4
10		leo 158	. . . . 5
11		df-i1 44	. . . . . . 7
12	11	ax-r1 35	. . . . . 6
13		ax-a1 30	. . . . . 6
14	12, 13	ax-r2 36	. . . . 5
15	10, 14	lbtr 139	. . . 4
16		leo 158	. . . . 5
17		df-i1 44	. . . . . . 7
18	17	ax-r1 35	. . . . . 6
19		ax-a1 30	. . . . . 6
20	18, 19	ax-r2 36	. . . . 5
21	16, 20	lbtr 139	. . . 4
22		or0 102	. . . . . 6
23	22	ax-r1 35	. . . . 5
24		oa3-2to2s.2	. . . . . . 7
25	5	lan 77	. . . . . . . . . . 11
26		omla 447	. . . . . . . . . . 11
27	25, 26	ax-r2 36	. . . . . . . . . 10
28	27	ax-r1 35	. . . . . . . . 9
29		ax-a1 30	. . . . . . . . . 10
30	29, 7	2an 79	. . . . . . . . 9
31	28, 30	ax-r2 36	. . . . . . . 8
32	11	lan 77	. . . . . . . . . . 11
33		omla 447	. . . . . . . . . . 11
34	32, 33	ax-r2 36	. . . . . . . . . 10
35	34	ax-r1 35	. . . . . . . . 9
36		ax-a1 30	. . . . . . . . . 10
37	36, 13	2an 79	. . . . . . . . 9
38	35, 37	ax-r2 36	. . . . . . . 8
39	31, 38	2or 72	. . . . . . 7
40	24, 39	ax-r2 36	. . . . . 6
41		an1 106	. . . . . . . 8
42	41	ax-r1 35	. . . . . . 7
43		ax-a1 30	. . . . . . . 8
44		0i1 273	. . . . . . . . . 10
45	44	ax-r1 35	. . . . . . . . 9
46	45, 19	ax-r2 36	. . . . . . . 8
47	43, 46	2an 79	. . . . . . 7
48	42, 47	ax-r2 36	. . . . . 6
49	40, 48	2or 72	. . . . 5
50	23, 49	ax-r2 36	. . . 4
51		oa3-2lema 978	. . . . 5
52		oa3-2to2s.1	. . . . 5
53	51, 52	bltr 138	. . . 4
54	9, 15, 21, 50, 29, 36, 43, 53	oa4to6 965	. . 3
55	1, 2, 3, 54	oa6to4 958	. 2
56		oa3-2lema 978	. 2
57		ancom 74	. . . . 5
58		an0 108	. . . . 5
59	57, 58	ax-r2 36	. . . 4
60	59	lor 70	. . 3
61		or0 102	. . 3
62	60, 61	ax-r2 36	. 2
63	55, 56, 62	le3tr2 141	1

Colors of variables: term

Syntax hints:   wb 1   wle 2  wn 4   wo 6   wa 7  wt 8  wf 9   wi1 12

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

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

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator