Theorem d3oa 975

Description: Derivation of 3-OA from OA distributive law.

Hypothesis

Ref	Expression
d3oa.1	f = ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))

Assertion

Ref	Expression
d3oa	((a ->1 c) ^ f) =< (b ->1 c)

Proof of Theorem d3oa

Step	Hyp	Ref	Expression
1		1oai1 803	. . 3 ((a ->1 c) ^ ((a ^ b)_|_ ->1 ((a ->1 c) ^ (b ->1 c)))) =< (b ->1 c)
2		2oath1i1 809	. . . 4 ((a ->1 c) ^ ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c)))) = ((a ->1 c) ^ (b ->1 c))
3		lear 153	. . . 4 ((a ->1 c) ^ (b ->1 c)) =< (b ->1 c)
4	2, 3	bltr 130	. . 3 ((a ->1 c) ^ ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c)))) =< (b ->1 c)
5	1, 4	le2or 160	. 2 (((a ->1 c) ^ ((a ^ b)_|_ ->1 ((a ->1 c) ^ (b ->1 c)))) v ((a ->1 c) ^ ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c))))) =< ((b ->1 c) v (b ->1 c))
6		id 58	. . . . 5 (((a ^ a) v ((a ->1 c) ^ (a ->1 c))) ^ ((b ^ a) v ((b ->1 c) ^ (a ->1 c)))) = (((a ^ a) v ((a ->1 c) ^ (a ->1 c))) ^ ((b ^ a) v ((b ->1 c) ^ (a ->1 c))))
7		id 58	. . . . 5 (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ a) v ((a ->1 c) ^ (a ->1 c))) ^ ((b ^ a) v ((b ->1 c) ^ (a ->1 c))))) = (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ a) v ((a ->1 c) ^ (a ->1 c))) ^ ((b ^ a) v ((b ->1 c) ^ (a ->1 c)))))
8		leid 140	. . . . 5 (a ->1 c) =< (a ->1 c)
9		df-i1 43	. . . . . . 7 ((a ^ b)_|_ ->1 ((a ->1 c) ^ (b ->1 c))) = ((a ^ b)_|__|_ v ((a ^ b)_|_ ^ ((a ->1 c) ^ (b ->1 c))))
10		ax-a1 29	. . . . . . . . . 10 (a ^ b) = (a ^ b)_|__|_
11	10	ax-r1 34	. . . . . . . . 9 (a ^ b)_|__|_ = (a ^ b)
12	11	bile 134	. . . . . . . 8 (a ^ b)_|__|_ =< (a ^ b)
13		lear 153	. . . . . . . 8 ((a ^ b)_|_ ^ ((a ->1 c) ^ (b ->1 c))) =< ((a ->1 c) ^ (b ->1 c))
14	12, 13	le2or 160	. . . . . . 7 ((a ^ b)_|__|_ v ((a ^ b)_|_ ^ ((a ->1 c) ^ (b ->1 c)))) =< ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))
15	9, 14	bltr 130	. . . . . 6 ((a ^ b)_|_ ->1 ((a ->1 c) ^ (b ->1 c))) =< ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))
16		leo 150	. . . . . 6 ((a ^ b) v ((a ->1 c) ^ (b ->1 c))) =< (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ a) v ((a ->1 c) ^ (a ->1 c))) ^ ((b ^ a) v ((b ->1 c) ^ (a ->1 c)))))
17	15, 16	letr 129	. . . . 5 ((a ^ b)_|_ ->1 ((a ->1 c) ^ (b ->1 c))) =< (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ a) v ((a ->1 c) ^ (a ->1 c))) ^ ((b ^ a) v ((b ->1 c) ^ (a ->1 c)))))
18		df-i2 44	. . . . . . . 8 ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c))) = (((a ->1 c) ^ (b ->1 c)) v ((a ^ b)_|__|_ ^ ((a ->1 c) ^ (b ->1 c))_|_))
19		ax-a2 30	. . . . . . . 8 (((a ->1 c) ^ (b ->1 c)) v ((a ^ b)_|__|_ ^ ((a ->1 c) ^ (b ->1 c))_|_)) = (((a ^ b)_|__|_ ^ ((a ->1 c) ^ (b ->1 c))_|_) v ((a ->1 c) ^ (b ->1 c)))
20	18, 19	ax-r2 35	. . . . . . 7 ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c))) = (((a ^ b)_|__|_ ^ ((a ->1 c) ^ (b ->1 c))_|_) v ((a ->1 c) ^ (b ->1 c)))
21		lea 152	. . . . . . . . 9 ((a ^ b)_|__|_ ^ ((a ->1 c) ^ (b ->1 c))_|_) =< (a ^ b)_|__|_
22	21, 11	lbtr 131	. . . . . . . 8 ((a ^ b)_|__|_ ^ ((a ->1 c) ^ (b ->1 c))_|_) =< (a ^ b)
23		leid 140	. . . . . . . 8 ((a ->1 c) ^ (b ->1 c)) =< ((a ->1 c) ^ (b ->1 c))
24	22, 23	le2or 160	. . . . . . 7 (((a ^ b)_|__|_ ^ ((a ->1 c) ^ (b ->1 c))_|_) v ((a ->1 c) ^ (b ->1 c))) =< ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))
25	20, 24	bltr 130	. . . . . 6 ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c))) =< ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))
26	25, 16	letr 129	. . . . 5 ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c))) =< (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ a) v ((a ->1 c) ^ (a ->1 c))) ^ ((b ^ a) v ((b ->1 c) ^ (a ->1 c)))))
27		leo 150	. . . . . 6 ((a ->1 c) ^ (b ->1 c)) =< (((a ->1 c) ^ (b ->1 c)) v ((a ^ b)_|__|_ ^ ((a ->1 c) ^ (b ->1 c))_|_))
28	18	ax-r1 34	. . . . . 6 (((a ->1 c) ^ (b ->1 c)) v ((a ^ b)_|__|_ ^ ((a ->1 c) ^ (b ->1 c))_|_)) = ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c)))
29	27, 28	lbtr 131	. . . . 5 ((a ->1 c) ^ (b ->1 c)) =< ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c)))
30	6, 7, 8, 17, 26, 29	ax-oadist 974	. . . 4 ((a ->1 c) ^ (((a ^ b)_|_ ->1 ((a ->1 c) ^ (b ->1 c))) v ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c))))) = (((a ->1 c) ^ ((a ^ b)_|_ ->1 ((a ->1 c) ^ (b ->1 c)))) v ((a ->1 c) ^ ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c)))))
31	30	ax-r1 34	. . 3 (((a ->1 c) ^ ((a ^ b)_|_ ->1 ((a ->1 c) ^ (b ->1 c)))) v ((a ->1 c) ^ ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c))))) = ((a ->1 c) ^ (((a ^ b)_|_ ->1 ((a ->1 c) ^ (b ->1 c))) v ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c)))))
32		u12lem 753	. . . . . . 7 (((a ^ b)_|_ ->1 ((a ->1 c) ^ (b ->1 c))) v ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c)))) = ((a ^ b)_|_ ->0 ((a ->1 c) ^ (b ->1 c)))
33		df-i0 42	. . . . . . 7 ((a ^ b)_|_ ->0 ((a ->1 c) ^ (b ->1 c))) = ((a ^ b)_|__|_ v ((a ->1 c) ^ (b ->1 c)))
34	32, 33	ax-r2 35	. . . . . 6 (((a ^ b)_|_ ->1 ((a ->1 c) ^ (b ->1 c))) v ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c)))) = ((a ^ b)_|__|_ v ((a ->1 c) ^ (b ->1 c)))
35	10	ax-r5 37	. . . . . . 7 ((a ^ b) v ((a ->1 c) ^ (b ->1 c))) = ((a ^ b)_|__|_ v ((a ->1 c) ^ (b ->1 c)))
36	35	ax-r1 34	. . . . . 6 ((a ^ b)_|__|_ v ((a ->1 c) ^ (b ->1 c))) = ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))
37	34, 36	ax-r2 35	. . . . 5 (((a ^ b)_|_ ->1 ((a ->1 c) ^ (b ->1 c))) v ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c)))) = ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))
38		d3oa.1	. . . . . 6 f = ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))
39	38	ax-r1 34	. . . . 5 ((a ^ b) v ((a