Theorem oadistc0 1001

Description: Pre-distributive law.

Hypotheses

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

Assertion

Ref	Expression
oadistc0	((a ->2 b) ^ ((b v c)_|_ v d)) = (((a ->2 b) ^ (b v c)_|_) v d)

Proof of Theorem oadistc0

Step	Hyp	Ref	Expression
1		ancom 68	. . . . 5 ((a ->2 c) ^ ((a ->2 b) ^ ((b v c)_|_ v d))) = (((a ->2 b) ^ ((b v c)_|_ v d)) ^ (a ->2 c))
2		oadistc0.1	. . . . . . . . 9 d =< ((a ->2 b) ^ (a ->2 c))
3	2	lelor 158	. . . . . . . 8 ((b v c)_|_ v d) =< ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))
4	3	lelan 159	. . . . . . 7 ((a ->2 b) ^ ((b v c)_|_ v d)) =< ((a ->2 b) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c))))
5		oal2 979	. . . . . . 7 ((a ->2 b) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)
6	4, 5	letr 129	. . . . . 6 ((a ->2 b) ^ ((b v c)_|_ v d)) =< (a ->2 c)
7	6	df2le2 128	. . . . 5 (((a ->2 b) ^ ((b v c)_|_ v d)) ^ (a ->2 c)) = ((a ->2 b) ^ ((b v c)_|_ v d))
8	1, 7	ax-r2 35	. . . 4 ((a ->2 c) ^ ((a ->2 b) ^ ((b v c)_|_ v d))) = ((a ->2 b) ^ ((b v c)_|_ v d))
9	8	ax-r1 34	. . 3 ((a ->2 b) ^ ((b v c)_|_ v d)) = ((a ->2 c) ^ ((a ->2 b) ^ ((b v c)_|_ v d)))
10		oadistc0.2	. . 3 ((a ->2 c) ^ ((a ->2 b) ^ ((b v c)_|_ v d))) =< (((a ->2 b) ^ (b v c)_|_) v d)
11	9, 10	bltr 130	. 2 ((a ->2 b) ^ ((b v c)_|_ v d)) =< (((a ->2 b) ^ (b v c)_|_) v d)
12		ledior 169	. . 3 (((a ->2 b) ^ (b v c)_|_) v d) =< (((a ->2 b) v d) ^ ((b v c)_|_ v d))
13		ax-a2 30	. . . . 5 ((a ->2 b) v d) = (d v (a ->2 b))
14		lea 152	. . . . . . 7 ((a ->2 b) ^ (a ->2 c)) =< (a ->2 b)
15	2, 14	letr 129	. . . . . 6 d =< (a ->2 b)
16	15	df-le2 123	. . . . 5 (d v (a ->2 b)) = (a ->2 b)
17	13, 16	ax-r2 35	. . . 4 ((a ->2 b) v d) = (a ->2 b)
18	17	ran 71	. . 3 (((a ->2 b) v d) ^ ((b v c)_|_ v d)) = ((a ->2 b) ^ ((b v c)_|_ v d))
19	12, 18	lbtr 131	. 2 (((a ->2 b) ^ (b v c)_|_) v d) =< ((a ->2 b) ^ ((b v c)_|_ v d))
20	11, 19	lebi 137	1 ((a ->2 b) ^ ((b v c)_|_ v d)) = (((a ->2 b) ^ (b v c)_|_) v d)

Syntax hints:   = wb 1   =< 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-3oa 978

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

metamath.org