Theorem oaidlem2 911

Description: Lemma for identity-like OA law.

Hypothesis

Ref	Expression
oaidlem2.1	((d v ((a ->1 c) ^ (b ->1 c)))_|_ v ((a ->1 c) ->1 (b ->1 c))) = 1

Assertion

Ref	Expression
oaidlem2	((a ->1 c) ^ (d v ((a ->1 c) ^ (b ->1 c)))) =< (b ->1 c)

Proof of Theorem oaidlem2

Step	Hyp	Ref	Expression
1		anidm 103	. . . . . . . . . 10 ((a ->1 c) ^ (a ->1 c)) = (a ->1 c)
2	1	ax-r1 34	. . . . . . . . 9 (a ->1 c) = ((a ->1 c) ^ (a ->1 c))
3	2	ran 71	. . . . . . . 8 ((a ->1 c) ^ (b ->1 c)) = (((a ->1 c) ^ (a ->1 c)) ^ (b ->1 c))
4		anass 69	. . . . . . . 8 (((a ->1 c) ^ (a ->1 c)) ^ (b ->1 c)) = ((a ->1 c) ^ ((a ->1 c) ^ (b ->1 c)))
5	3, 4	ax-r2 35	. . . . . . 7 ((a ->1 c) ^ (b ->1 c)) = ((a ->1 c) ^ ((a ->1 c) ^ (b ->1 c)))
6		leor 151	. . . . . . . 8 ((a ->1 c) ^ (b ->1 c)) =< (d v ((a ->1 c) ^ (b ->1 c)))
7	6	lelan 159	. . . . . . 7 ((a ->1 c) ^ ((a ->1 c) ^ (b ->1 c))) =< ((a ->1 c) ^ (d v ((a ->1 c) ^ (b ->1 c))))
8	5, 7	bltr 130	. . . . . 6 ((a ->1 c) ^ (b ->1 c)) =< ((a ->1 c) ^ (d v ((a ->1 c) ^ (b ->1 c))))
9	8	df-le2 123	. . . . 5 (((a ->1 c) ^ (b ->1 c)) v ((a ->1 c) ^ (d v ((a ->1 c) ^ (b ->1 c))))) = ((a ->1 c) ^ (d v ((a ->1 c) ^ (b ->1 c))))
10		ax-a3 31	. . . . . 6 (((d v ((a ->1 c) ^ (b ->1 c)))_|_ v (a ->1 c)_|_) v ((a ->1 c) ^ (b ->1 c))) = ((d v ((a ->1 c) ^ (b ->1 c)))_|_ v ((a ->1 c)_|_ v ((a ->1 c) ^ (b ->1 c))))
11		ax-a2 30	. . . . . . . 8 ((d v ((a ->1 c) ^ (b ->1 c)))_|_ v (a ->1 c)_|_) = ((a ->1 c)_|_ v (d v ((a ->1 c) ^ (b ->1 c)))_|_)
12		oran3 85	. . . . . . . 8 ((a ->1 c)_|_ v (d v ((a ->1 c) ^ (b ->1 c)))_|_) = ((a ->1 c) ^ (d v ((a ->1 c) ^ (b ->1 c))))_|_
13	11, 12	ax-r2 35	. . . . . . 7 ((d v ((a ->1 c) ^ (b ->1 c)))_|_ v (a ->1 c)_|_) = ((a ->1 c) ^ (d v ((a ->1 c) ^ (b ->1 c))))_|_
14	13	ax-r5 37	. . . . . 6 (((d v ((a ->1 c) ^ (b ->1 c)))_|_ v (a ->1 c)_|_) v ((a ->1 c) ^ (b ->1 c))) = (((a ->1 c) ^ (d v ((a ->1 c) ^ (b ->1 c))))_|_ v ((a ->1 c) ^ (b ->1 c)))
15		df-i1 43	. . . . . . . . 9 ((a ->1 c) ->1 (b ->1 c)) = ((a ->1 c)_|_ v ((a ->1 c) ^ (b ->1 c)))
16	15	lor 66	. . . . . . . 8 ((d v ((a ->1 c) ^ (b ->1 c)))_|_ v ((a ->1 c) ->1 (b ->1 c))) = ((d v ((a ->1 c) ^ (b ->1 c)))_|_ v ((a ->1 c)_|_ v ((a ->1 c) ^ (b ->1 c))))
17	16	ax-r1 34	. . . . . . 7 ((d v ((a ->1 c) ^ (b ->1 c)))_|_ v ((a ->1 c)_|_ v ((a ->1 c) ^ (b ->1 c)))) = ((d v ((a ->1 c) ^ (b ->1 c)))_|_ v ((a ->1 c) ->1 (b ->1 c)))
18		oaidlem2.1	. . . . . . 7 ((d v ((a ->1 c) ^ (b ->1 c)))_|_ v ((a ->1 c) ->1 (b ->1 c))) = 1
19	17, 18	ax-r2 35	. . . . . 6 ((d v ((a ->1 c) ^ (b ->1 c)))_|_ v ((a ->1 c)_|_ v ((a ->1 c) ^ (b ->1 c)))) = 1
20	10, 14, 19	3tr2 61	. . . . 5 (((a ->1 c) ^ (d v ((a ->1 c) ^ (b ->1 c))))_|_ v ((a ->1 c) ^ (b ->1 c))) = 1
21	9, 20	lem3.1 425	. . . 4 ((a ->1 c) ^ (b ->1 c)) = ((a ->1 c) ^ (d v ((a ->1 c) ^ (b ->1 c))))
22	21	ax-r1 34	. . 3 ((a ->1 c) ^ (d v ((a ->1 c) ^ (b ->1 c)))) = ((a ->1 c) ^ (b ->1 c))
23	22	bile 134	. 2 ((a ->1 c) ^ (d v ((a ->1 c) ^ (b ->1 c)))) =< ((a ->1 c) ^ (b ->1 c))
24		lear 153	. 2 ((a ->1 c) ^ (b ->1 c)) =< (b ->1 c)
25	23, 24	letr 129	1 ((a ->1 c) ^ (d v ((a ->1 c) ^ (b ->1 c)))) =< (b ->1 c)

Syntax hints:   = wb 1   =< wle 2  _|_wn 4   v wo 6   ^ wa 7  1wt 9   ->1 wi1 13

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

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

metamath.org