Theorem 1oa 802

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 153	. . 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 74	. . . . 5 (a_|_ ^ (b_|_ ^ c_|_)) = (b_|_ ^ (a_|_ ^ c_|_))
3		lear 153	. . . . . 6 (b_|_ ^ (a_|_ ^ c_|_)) =< (a_|_ ^ c_|_)
4	3	lerr 142	. . . . 5 (b_|_ ^ (a_|_ ^ c_|_)) =< (c v (a_|_ ^ c_|_))
5	2, 4	bltr 130	. . . 4 (a_|_ ^ (b_|_ ^ c_|_)) =< (c v (a_|_ ^ c_|_))
6		leid 140	. . . 4 (c v (a_|_ ^ c_|_)) =< (c v (a_|_ ^ c_|_))
7	5, 6	lel2or 162	. . 3 ((a_|_ ^ (b_|_ ^ c_|_)) v (c v (a_|_ ^ c_|_))) =< (c v (a_|_ ^ c_|_))
8	1, 7	letr 129	. 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 43	. . . 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 70	. . 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 74	. . . . . 6 ((a ->2 b) ^ ((b v c) ^ (a ->2 c))) = ((b v c) ^ ((a ->2 b) ^ (a ->2 c)))
12	11	ax-r1 34	. . . . 5 ((b v c) ^ ((a ->2 b) ^ (a ->2 c))) = ((a ->2 b) ^ ((b v c) ^ (a ->2 c)))
13		coman1 177	. . . . 5 ((a ->2 b) ^ ((b v c) ^ (a ->2 c))) C (a ->2 b)
14	12, 13	bctr 173	. . . 4 ((b v c) ^ ((a ->2 b) ^ (a ->2 c))) C (a ->2 b)
15		coman1 177	. . . . 5 ((b v c) ^ ((a ->2 b) ^ (a ->2 c))) C (b v c)
16	15	comcom2 175	. . . 4 ((b v c) ^ ((a ->2 b) ^ (a ->2 c))) C (b v c)_|_
17	14, 16	fh2c 459	. . 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 44	. . . . . . 7 (a ->2 b) = (b v (a_|_ ^ b_|_))
19		anor3 82	. . . . . . . 8 (b_|_ ^ c_|_) = (b v c)_|_
20	19	ax-r1 34	. . . . . . 7 (b v c)_|_ = (b_|_ ^ c_|_)
21	18, 20	2an 72	. . . . . 6 ((a ->2 b) ^ (b v c)_|_) = ((b v (a_|_ ^ b_|_)) ^ (b_|_ ^ c_|_))
22		comid 179	. . . . . . . . . . 11 b C b
23	22	comcom3 436	. . . . . . . . . 10 b_|_ C b
24		comanr2 447	. . . . . . . . . 10 b_|_ C (a_|_ ^ b_|_)
25	23, 24	fh1r 455	. . . . . . . . 9 ((b v (a_|_ ^ b_|_)) ^ b_|_) = ((b ^ b_|_) v ((a_|_ ^ b_|_) ^ b_|_))
26		dff 93	. . . . . . . . . . 11 0 = (b ^ b_|_)
27	26	ax-r1 34	. . . . . . . . . 10 (b ^ b_|_) = 0
28		anass 69	. . . . . . . . . . 11 ((a_|_ ^ b_|_) ^ b_|_) = (a_|_ ^ (b_|_ ^ b_|_))
29		anidm 103	. . . . . . . . . . . 12 (b_|_ ^ b_|_) = b_|_
30	29	lan 70	. . . . . . . . . . 11 (a_|_ ^ (b_|_ ^ b_|_)) = (a_|_ ^ b_|_)
31	28, 30	ax-r2 35	. . . . . . . . . 10 ((a_|_ ^ b_|_) ^ b_|_) = (a_|_ ^ b_|_)
32	27, 31	2or 67	. . . . . . . . 9 ((b ^ b_|_) v ((a_|_ ^ b_|_) ^ b_|_)) = (0 v (a_|_ ^ b_|_))
33		ax-a2 30	. . . . . . . . . 10 (0 v (a_|_ ^ b_|_)) = ((a_|_ ^ b_|_) v 0)
34		or0 94	. . . . . . . . . 10 ((a_|_ ^ b_|_) v 0) = (a_|_ ^ b_|_)
35	33, 34	ax-r2 35	. . . . . . . . 9 (0 v (a_|_ ^ b_|_)) = (a_|_ ^ b_|_)
36	25, 32, 35	3tr 62	. . . . . . . 8 ((b v (a_|_ ^ b_|_)) ^ b_|_) = (a_|_ ^ b_|_)
37	36	ran 71	. . . . . . 7 (((b v (a_|_ ^ b_|_)) ^ b_|_) ^ c_|_) = ((a_|_ ^ b_|_) ^ c_|_)
38		anass 69	. . . . . . 7 (((b v (a_|_ ^ b_|_)) ^ b_|_) ^ c_|_) = ((b v (a_|_ ^ b_|_)) ^ (b_|_ ^ c_|_))
39		anass 69	. . . . . . 7 ((a_|_ ^ b_|_) ^ c_|_) = (a_|_ ^ (b_|_ ^ c_|_))
40	37, 38, 39	3tr2 61	. . . . . 6 ((b v (a_|_ ^ b_|_)) ^ (b_|_ ^ c_|_)) = (a_|_ ^ (b_|_ ^ c_|_))
41	21, 40	ax-r2 35	. . . . 5 ((a ->2 b) ^ (b v c)_|_) = (a_|_ ^ (b_|_ ^ c_|_))
42		an12 74	. . . . . 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 69	. . . . . . . . 9 (((a ->2 b) ^ (a ->2 b)) ^ (a ->2 c)) = ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c)))
44	43	ax-r1 34	. . . . . . . 8 ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c))) = (((a ->2 b) ^ (a ->2 b)) ^ (a ->2 c))
45		anidm 103	. . . . . . . . . 10 ((a ->2 b) ^ (a ->2 b)) = (a ->2 b)
46	45, 18	ax-r2 35	. . . . . . . . 9 ((a ->2 b) ^ (a ->2 b)) = (b v (a_|_ ^ b_|_))
47		df-i2 44	. . . . . . . . 9 (a ->2 c) = (c v (a_|_ ^ c_|_))
48	46, 47	2an 72	. . . . . . . 8 (((a ->2 b) ^ (a ->2 b)) ^ (a ->2 c)) = ((b v (a_|_ ^ b_|_)) ^ (c v (a_|_ ^ c_|_)))
49	44, 48	ax-r2 35	. . . . . . 7 ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c))) = ((b v (a_|_ ^ b_|_)) ^ (c v (a_|_ ^ c_|_)))
50	49	lan 70	. . . . . 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 35	. . . . 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 67	. . . 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 34	. . . . . . . 8 (a_|_ ^ (b_|_ ^ c_|_)) = ((a_|_ ^ b_|_) ^ c_|_)
54		lea 152	. . . . . . . . . 10 ((a_|_ ^ b_|_) ^ c_|_) =< (a_|_ ^ b_|_)
55	54	lerr 142	. . . . . . . . 9 ((a_|_ ^ b_|_) ^ c_|_) =< (b v (a_|_ ^ b_|_))
56	55	lecom 172	. . . . . . . 8 ((a_|_ ^ b_|_) ^ c_|_) C (b v (a_|_ ^ b_|_))
57	53, 56	bctr 173	. . . . . . 7 (a_|_ ^ (b_|_ ^ c_|_)) C (b v (a_|_ ^ b_|_))
58	4	lecom 172	. . . . . . . 8 (b_|_ ^ (a_|_ ^ c_|_)) C (c v (a_|_ ^ c_|_))
59	2, 58	bctr 173	. . . . . . 7 (a_|_ ^ (b_|_ ^ c_|_)) C (c v (a_|_ ^ c_|_))
60	57, 59	fh3 453	. . . . . 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 (c v (a_|_ ^ c_|_))))
61	60	lan 70	. . . . 5 (((a_|_ ^ (b_|_ ^ c_|_)) v (b