Theorem oale 811

Description: Relation for studying OA.

Assertion

Ref	Expression
oale	((a ->2 b) ^ ((b v c) v ((a ->2 b) ^ (a ->2 c)))_|_) =< (a ->2 c)

Proof of Theorem oale

Step	Hyp	Ref	Expression
1		df-i2 44	. . . . . . 7 ((b v c) ->2 ((a ->2 b) ^ (a ->2 c))) = (((a ->2 b) ^ (a ->2 c)) v ((b v c)_|_ ^ ((a ->2 b) ^ (a ->2 c))_|_))
2	1	lan 70	. . . . . 6 ((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))) = ((a ->2 b) ^ (((a ->2 b) ^ (a ->2 c)) v ((b v c)_|_ ^ ((a ->2 b) ^ (a ->2 c))_|_)))
3		coman1 177	. . . . . . 7 ((a ->2 b) ^ (a ->2 c)) C (a ->2 b)
4		comanr2 447	. . . . . . . 8 ((a ->2 b) ^ (a ->2 c))_|_ C ((b v c)_|_ ^ ((a ->2 b) ^ (a ->2 c))_|_)
5	4	comcom6 441	. . . . . . 7 ((a ->2 b) ^ (a ->2 c)) C ((b v c)_|_ ^ ((a ->2 b) ^ (a ->2 c))_|_)
6	3, 5	fh2 452	. . . . . 6 ((a ->2 b) ^ (((a ->2 b) ^ (a ->2 c)) v ((b v c)_|_ ^ ((a ->2 b) ^ (a ->2 c))_|_))) = (((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c))) v ((a ->2 b) ^ ((b v c)_|_ ^ ((a ->2 b) ^ (a ->2 c))_|_)))
7		anass 69	. . . . . . . . . 10 (((a ->2 b) ^ (a ->2 b)) ^ (a ->2 c)) = ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c)))
8	7	ax-r1 34	. . . . . . . . 9 ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c))) = (((a ->2 b) ^ (a ->2 b)) ^ (a ->2 c))
9		anidm 103	. . . . . . . . . 10 ((a ->2 b) ^ (a ->2 b)) = (a ->2 b)
10	9	ran 71	. . . . . . . . 9 (((a ->2 b) ^ (a ->2 b)) ^ (a ->2 c)) = ((a ->2 b) ^ (a ->2 c))
11	8, 10	ax-r2 35	. . . . . . . 8 ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c))) = ((a ->2 b) ^ (a ->2 c))
12		anor3 82	. . . . . . . . 9 ((b v c)_|_ ^ ((a ->2 b) ^ (a ->2 c))_|_) = ((b v c) v ((a ->2 b) ^ (a ->2 c)))_|_
13	12	lan 70	. . . . . . . 8 ((a ->2 b) ^ ((b v c)_|_ ^ ((a ->2 b) ^ (a ->2 c))_|_)) = ((a ->2 b) ^ ((b v c) v ((a ->2 b) ^ (a ->2 c)))_|_)
14	11, 13	2or 67	. . . . . . 7 (((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c))) v ((a ->2 b) ^ ((b v c)_|_ ^ ((a ->2 b) ^ (a ->2 c))_|_))) = (((a ->2 b) ^ (a ->2 c)) v ((a ->2 b) ^ ((b v c) v ((a ->2 b) ^ (a ->2 c)))_|_))
15		ax-a2 30	. . . . . . 7 (((a ->2 b) ^ (a ->2 c)) v ((a ->2 b) ^ ((b v c) v ((a ->2 b) ^ (a ->2 c)))_|_)) = (((a ->2 b) ^ ((b v c) v ((a ->2 b) ^ (a ->2 c)))_|_) v ((a ->2 b) ^ (a ->2 c)))
16	14, 15	ax-r2 35	. . . . . 6 (((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c))) v ((a ->2 b) ^ ((b v c)_|_ ^ ((a ->2 b) ^ (a ->2 c))_|_))) = (((a ->2 b) ^ ((b v c) v ((a ->2 b) ^ (a ->2 c)))_|_) v ((a ->2 b) ^ (a ->2 c)))
17	2, 6, 16	3tr 62	. . . . 5 ((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))) = (((a ->2 b) ^ ((b v c) v ((a ->2 b) ^ (a ->2 c)))_|_) v ((a ->2 b) ^ (a ->2 c)))
18	17	ax-r1 34	. . . 4 (((a ->2 b) ^ ((b v c) v ((a ->2 b) ^ (a ->2 c)))_|_) v ((a ->2 b) ^ (a ->2 c))) = ((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c))))
19		2oath1 808	. . . 4 ((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))) = ((a ->2 b) ^ (a ->2 c))
20	18, 19	ax-r2 35	. . 3 (((a ->2 b) ^ ((b v c) v ((a ->2 b) ^ (a ->2 c)))_|_) v ((a ->2 b) ^ (a ->2 c))) = ((a ->2 b) ^ (a ->2 c))
21	20	df-le1 122	. 2 ((a ->2 b) ^ ((b v c) v ((a ->2 b) ^ (a ->2 c)))_|_) =< ((a ->2 b) ^ (a ->2 c))
22		lear 153	. 2 ((a ->2 b) ^ (a ->2 c)) =< (a ->2 c)
23	21, 22	letr 129	1 ((a ->2 b) ^ ((b v c) v ((a ->2 b) ^ (a ->2 c)))_|_) =< (a ->2 c)

Syntax hints:   =< wle 2  _|_wn 4   v wo 6   ^ wa 7   ->2 wi2 14

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-r3 421

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i2 44  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org