Theorem 1oa 820

Description: Orthoarguesian-like law with ->1 instead of ->0 but true in all OMLs.

Assertion

Ref	Expression
1oa	((a ->2 b) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)

Proof of Theorem 1oa

Step	Hyp	Ref	Expression
1		lear 161	. . 3 ((((a' ^ (b' ^ c')) v (b v c)) ^ ((a' ^ (b' ^ c')) v (b v (a' ^ b')))) ^ ((a' ^ (b' ^ c')) v (c v (a' ^ c')))) =< ((a' ^ (b' ^ c')) v (c v (a' ^ c')))
2		an12 81	. . . . 5 (a' ^ (b' ^ c')) = (b' ^ (a' ^ c'))
3		lear 161	. . . . . 6 (b' ^ (a' ^ c')) =< (a' ^ c')
4	3	lerr 150	. . . . 5 (b' ^ (a' ^ c')) =< (c v (a' ^ c'))
5	2, 4	bltr 138	. . . 4 (a' ^ (b' ^ c')) =< (c v (a' ^ c'))
6		leid 148	. . . 4 (c v (a' ^ c')) =< (c v (a' ^ c'))
7	5, 6	lel2or 170	. . 3 ((a' ^ (b' ^ c')) v (c v (a' ^ c'))) =< (c v (a' ^ c'))
8	1, 7	letr 137	. 2 ((((a' ^ (b' ^ c')) v (b v c)) ^ ((a' ^ (b' ^ c')) v (b v (a' ^ b')))) ^ ((a' ^ (b' ^ c')) v (c v (a' ^ c')))) =< (c v (a' ^ c'))
9		df-i1 44	. . . 4 ((b v c) ->1 ((a ->2 b) ^ (a ->2 c))) = ((b v c)' v ((b v c) ^ ((a ->2 b) ^ (a ->2 c))))
10	9	lan 77	. . 3 ((a ->2 b) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))) = ((a ->2 b) ^ ((b v c)' v ((b v c) ^ ((a ->2 b) ^ (a ->2 c)))))
11		an12 81	. . . . . 6 ((a ->2 b) ^ ((b v c) ^ (a ->2 c))) = ((b v c) ^ ((a ->2 b) ^ (a ->2 c)))
12	11	ax-r1 35	. . . . 5 ((b v c) ^ ((a ->2 b) ^ (a ->2 c))) = ((a ->2 b) ^ ((b v c) ^ (a ->2 c)))
13		coman1 185	. . . . 5 ((a ->2 b) ^ ((b v c) ^ (a ->2 c))) C (a ->2 b)
14	12, 13	bctr 181	. . . 4 ((b v c) ^ ((a ->2 b) ^ (a ->2 c))) C (a ->2 b)
15		coman1 185	. . . . 5 ((b v c) ^ ((a ->2 b) ^ (a ->2 c))) C (b v c)
16	15	comcom2 183	. . . 4 ((b v c) ^ ((a ->2 b) ^ (a ->2 c))) C (b v c)'
17	14, 16	fh2c 477	. . 3 ((a ->2 b) ^ ((b v c)' v ((b v c) ^ ((a ->2 b) ^ (a ->2 c))))) = (((a ->2 b) ^ (b v c)') v ((a ->2 b) ^ ((b v c) ^ ((a ->2 b) ^ (a ->2 c)))))
18		df-i2 45	. . . . . . 7 (a ->2 b) = (b v (a' ^ b'))
19		anor3 90	. . . . . . . 8 (b' ^ c') = (b v c)'
20	19	ax-r1 35	. . . . . . 7 (b v c)' = (b' ^ c')
21	18, 20	2an 79	. . . . . 6 ((a ->2 b) ^ (b v c)') = ((b v (a' ^ b')) ^ (b' ^ c'))
22		comid 187	. . . . . . . . . . 11 b C b
23	22	comcom3 454	. . . . . . . . . 10 b' C b
24		comanr2 465	. . . . . . . . . 10 b' C (a' ^ b')
25	23, 24	fh1r 473	. . . . . . . . 9 ((b v (a' ^ b')) ^ b') = ((b ^ b') v ((a' ^ b') ^ b'))
26		dff 101	. . . . . . . . . . 11 0 = (b ^ b')
27	26	ax-r1 35	. . . . . . . . . 10 (b ^ b') = 0
28		anass 76	. . . . . . . . . . 11 ((a' ^ b') ^ b') = (a' ^ (b' ^ b'))
29		anidm 111	. . . . . . . . . . . 12 (b' ^ b') = b'
30	29	lan 77	. . . . . . . . . . 11 (a' ^ (b' ^ b')) = (a' ^ b')
31	28, 30	ax-r2 36	. . . . . . . . . 10 ((a' ^ b') ^ b') = (a' ^ b')
32	27, 31	2or 72	. . . . . . . . 9 ((b ^ b') v ((a' ^ b') ^ b')) = (0 v (a' ^ b'))
33		ax-a2 31	. . . . . . . . . 10 (0 v (a' ^ b')) = ((a' ^ b') v 0)
34		or0 102	. . . . . . . . . 10 ((a' ^ b') v 0) = (a' ^ b')
35	33, 34	ax-r2 36	. . . . . . . . 9 (0 v (a' ^ b')) = (a' ^ b')
36	25, 32, 35	3tr 65	. . . . . . . 8 ((b v (a' ^ b')) ^ b') = (a' ^ b')
37	36	ran 78	. . . . . . 7 (((b v (a' ^ b')) ^ b') ^ c') = ((a' ^ b') ^ c')
38		anass 76	. . . . . . 7 (((b v (a' ^ b')) ^ b') ^ c') = ((b v (a' ^ b')) ^ (b' ^ c'))
39		anass 76	. . . . . . 7 ((a' ^ b') ^ c') = (a' ^ (b' ^ c'))
40	37, 38, 39	3tr2 64	. . . . . 6 ((b v (a' ^ b')) ^ (b' ^ c')) = (a' ^ (b' ^ c'))
41	21, 40	ax-r2 36	. . . . 5 ((a ->2 b) ^ (b v c)') = (a' ^ (b' ^ c'))
42		an12 81	. . . . . 6 ((a ->2 b) ^ ((b v c) ^ ((a ->2 b) ^ (a ->2 c)))) = ((b v c) ^ ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c))))
43		anass 76	. . . . . . . . 9 (((a ->2 b) ^ (a ->2 b)) ^ (a ->2 c)) = ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c)))
44	43	ax-r1 35	. . . . . . . 8 ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c))) = (((a ->2 b) ^ (a ->2 b)) ^ (a ->2 c))
45		anidm 111	. . . . . . . . . 10 ((a ->2 b) ^ (a ->2 b)) = (a ->2 b)
46	45, 18	ax-r2 36	. . . . . . . . 9 ((a ->2 b) ^ (a ->2 b)) = (b v (a' ^ b'))
47		df-i2 45	. . . . . . . . 9 (a ->2 c) = (c v (a' ^ c'))
48	46, 47	2an 79	. . . . . . . 8 (((a ->2 b) ^ (a ->2 b)) ^ (a ->2 c)) = ((b v (a' ^ b')) ^ (c v (a' ^ c')))
49	44, 48	ax-r2 36	. . . . . . 7 ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c))) = ((b v (a' ^ b')) ^ (c v (a' ^ c')))
50	49	lan 77	. . . . . 6 ((b v c) ^ ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c)))) = ((b v c) ^ ((b v (a' ^ b')) ^ (c v (a' ^ c'))))
51	42, 50	ax-r2 36	. . . . 5 ((a ->2 b) ^ ((b v c) ^ ((a ->2 b) ^ (a ->2 c)))) = ((b v c) ^ ((b v (a' ^ b')) ^ (c v (a' ^ c'))))
52	41, 51	2or 72	. . . 4 (((a ->2 b) ^ (b v c)') v ((a ->2 b) ^ ((b v c) ^ ((a ->2 b) ^ (a ->2 c))))) = ((a' ^ (b' ^ c')) v ((b v c) ^ ((b v (a' ^ b')) ^ (c v (a' ^ c')))))
53	39	ax-r1 35	. . . . . . . 8 (a' ^ (b' ^ c')) = ((a' ^ b') ^ c')
54		lea 160	. . . . . . . . . 10 ((a' ^ b') ^ c') =< (a' ^ b')
55	54	lerr 150	. . . . . . . . 9 ((a' ^ b') ^ c') =< (b v (a' ^ b'))
56	55	lecom 180	. . . . . . . 8 ((a' ^ b') ^ c') C (b v (a' ^ b'))
57	53, 56	bctr 181	. . . . . . 7 (a' ^ (b' ^ c')) C (b v (a' ^ b'))
58	4	lecom 180	. . . . . . . 8 (b' ^ (a' ^ c')) C (c v (a' ^ c'))
59	2, 58	bctr 181	. . . . . . 7 (a' ^ (b' ^ c')) C (c v (a' ^ c'))
60	57, 59	fh3 471	. . . . . 6 ((a' ^ (b' ^ c')) v ((b v (a' ^ b')) ^ (c v (a' ^ c')))) = (((a' ^ (b' ^ c')) v (b v (a' ^ b'))) ^ ((a' ^ (b' ^ c')) v