Theorem oalem1 985

Description: Lemma

Assertion

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

Proof of Theorem oalem1

Step	Hyp	Ref	Expression
1		anidm 103	. . . . . . . . 9 (b_|_ ^ b_|_) = b_|_
2	1	ran 71	. . . . . . . 8 ((b_|_ ^ b_|_) ^ c_|_) = (b_|_ ^ c_|_)
3	2	ax-r1 34	. . . . . . 7 (b_|_ ^ c_|_) = ((b_|_ ^ b_|_) ^ c_|_)
4		anor3 82	. . . . . . 7 (b_|_ ^ c_|_) = (b v c)_|_
5		an32 76	. . . . . . . 8 ((b_|_ ^ b_|_) ^ c_|_) = ((b_|_ ^ c_|_) ^ b_|_)
6	4	ran 71	. . . . . . . 8 ((b_|_ ^ c_|_) ^ b_|_) = ((b v c)_|_ ^ b_|_)
7	5, 6	ax-r2 35	. . . . . . 7 ((b_|_ ^ b_|_) ^ c_|_) = ((b v c)_|_ ^ b_|_)
8	3, 4, 7	3tr2 61	. . . . . 6 (b v c)_|_ = ((b v c)_|_ ^ b_|_)
9	8	ran 71	. . . . 5 ((b v c)_|_ ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))))) = (((b v c)_|_ ^ b_|_) ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c))))))
10		anass 69	. . . . . 6 (((b v c)_|_ ^ b_|_) ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))))) = ((b v c)_|_ ^ (b_|_ ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))))))
11		oalii 982	. . . . . . 7 (b_|_ ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))))) =< a_|_
12	11	lelan 159	. . . . . 6 ((b v c)_|_ ^ (b_|_ ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c))))))) =< ((b v c)_|_ ^ a_|_)
13	10, 12	bltr 130	. . . . 5 (((b v c)_|_ ^ b_|_) ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))))) =< ((b v c)_|_ ^ a_|_)
14	9, 13	bltr 130	. . . 4 ((b v c)_|_ ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))))) =< ((b v c)_|_ ^ a_|_)
15		ancom 68	. . . 4 ((b v c)_|_ ^ a_|_) = (a_|_ ^ (b v c)_|_)
16	14, 15	lbtr 131	. . 3 ((b v c)_|_ ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))))) =< (a_|_ ^ (b v c)_|_)
17	16	lelor 158	. 2 ((b v c) v ((b v c)_|_ ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c))))))) =< ((b v c) v (a_|_ ^ (b v c)_|_))
18		df-i2 44	. . 3 (a ->2 (b v c)) = ((b v c) v (a_|_ ^ (b v c)_|_))
19	18	ax-r1 34	. 2 ((b v c) v (a_|_ ^ (b v c)_|_)) = (a ->2 (b v c))
20	17, 19	lbtr 131	1 ((b v c) v ((b v c)_|_ ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c))))))) =< (a ->2 (b v 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-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-r3 421  ax-3oa 978

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-i2 44  df-le1 122  df-le2 123

metamath.org