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

---

Theorem test 802

Description: Part of an attempt to crack a potential Kalmbach axiom.

Assertion

Ref	Expression
test

---

Proof of Theorem test

Step	Hyp	Ref	Expression
1		oran3 93	. . . . 5
2	1	lor 70	. . . 4
3	2	ran 78	. . 3
4	3	ax-r5 38	. 2
5		comor1 461	. . . . . . 7
6	5	comcom2 183	. . . . . 6
7		comor2 462	. . . . . . 7
8	7	comcom7 460	. . . . . 6
9	6, 8	com2an 484	. . . . 5
10	6, 8	com2or 483	. . . . . 6
11	5, 10	com2an 484	. . . . 5
12	9, 11	com2or 483	. . . 4
13	5, 8	com2or 483	. . . . 5
14	6, 13	com2an 484	. . . 4
15	12, 14	fh4r 476	. . 3
16		ax-a3 32	. . . . . . 7
17	16	ax-r1 35	. . . . . 6
18		ax-a2 31	. . . . . . 7
19		anor2 89	. . . . . . . . . . 11
20	19	lor 70	. . . . . . . . . 10
21		df-t 41	. . . . . . . . . . 11
22	21	ax-r1 35	. . . . . . . . . 10
23	20, 22	ax-r2 36	. . . . . . . . 9
24	23	lor 70	. . . . . . . 8
25		or1 104	. . . . . . . 8
26	24, 25	ax-r2 36	. . . . . . 7
27	18, 26	ax-r2 36	. . . . . 6
28	17, 27	ax-r2 36	. . . . 5
29		ax-a3 32	. . . . . . 7
30	29	ax-r1 35	. . . . . 6
31		ax-a2 31	. . . . . . . . 9
32		leor 159	. . . . . . . . . . 11
33	32	lelan 167	. . . . . . . . . 10
34	33	df-le2 131	. . . . . . . . 9
35	31, 34	ax-r2 36	. . . . . . . 8
36	35	ax-r5 38	. . . . . . 7
37		coman1 185	. . . . . . . . . 10
38	37	comcom7 460	. . . . . . . . 9
39		comor1 461	. . . . . . . . . . 11
40	39	comcom7 460	. . . . . . . . . . . 12
41		comor2 462	. . . . . . . . . . . 12
42	40, 41	com2or 483	. . . . . . . . . . 11
43	39, 42	com2an 484	. . . . . . . . . 10
44	43	comcom 453	. . . . . . . . 9
45	38, 44	fh3 471	. . . . . . . 8
46		ax-a2 31	. . . . . . . . . 10
47		oml 445	. . . . . . . . . 10
48	46, 47	ax-r2 36	. . . . . . . . 9
49		or12 80	. . . . . . . . . 10
50		ax-a3 32	. . . . . . . . . . . 12
51	50	ax-r1 35	. . . . . . . . . . 11
52		orabs 120	. . . . . . . . . . . 12
53	52	ax-r5 38	. . . . . . . . . . 11
54	51, 53	ax-r2 36	. . . . . . . . . 10
55	49, 54	ax-r2 36	. . . . . . . . 9
56	48, 55	2an 79	. . . . . . . 8
57	45, 56	ax-r2 36	. . . . . . 7
58	36, 57	ax-r2 36	. . . . . 6
59	30, 58	ax-r2 36	. . . . 5
60	28, 59	2an 79	. . . 4
61		ancom 74	. . . . 5
62		an1 106	. . . . 5
63	61, 62	ax-r2 36	. . . 4
64	60, 63	ax-r2 36	. . 3
65	15, 64	ax-r2 36	. 2
66	4, 65	ax-r2 36	1

Colors of variables: term

Syntax hints:   wb 1  wn 4   wo 6   wa 7  wt 8

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-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator