Theorem d3oa 995

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 821	. . 3 ((a ->1 c) ^ ((a ^ b)' ->1 ((a ->1 c) ^ (b ->1 c)))) =< (b ->1 c)
2		2oath1i1 827	. . . 4 ((a ->1 c) ^ ((a ^ b)' ->2 ((a ->1 c) ^ (b ->1 c)))) = ((a ->1 c) ^ (b ->1 c))
3		lear 161	. . . 4 ((a ->1 c) ^ (b ->1 c)) =< (b ->1 c)
4	2, 3	bltr 138	. . 3 ((a ->1 c) ^ ((a ^ b)' ->2 ((a ->1 c) ^ (b ->1 c)))) =< (b ->1 c)
5	1, 4	le2or 168	. 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 59	. . . . 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 59	. . . . 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 148	. . . . 5 (a ->1 c) =< (a ->1 c)
9		df-i1 44	. . . . . . 7 ((a ^ b)' ->1 ((a ->1 c) ^ (b ->1 c))) = ((a ^ b)'' v ((a ^ b)' ^ ((a ->1 c) ^ (b ->1 c))))
10		ax-a1 30	. . . . . . . . . 10 (a ^ b) = (a ^ b)''
11	10	ax-r1 35	. . . . . . . . 9 (a ^ b)'' = (a ^ b)
12	11	bile 142	. . . . . . . 8 (a ^ b)'' =< (a ^ b)
13		lear 161	. . . . . . . 8 ((a ^ b)' ^ ((a ->1 c) ^ (b ->1 c))) =< ((a ->1 c) ^ (b ->1 c))
14	12, 13	le2or 168	. . . . . . 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 138	. . . . . 6 ((a ^ b)' ->1 ((a ->1 c) ^ (b ->1 c))) =< ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))
16		leo 158	. . . . . 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 137	. . . . 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 45	. . . . . . . 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 31	. . . . . . . 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 36	. . . . . . 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 160	. . . . . . . . 9 ((a ^ b)'' ^ ((a ->1 c) ^ (b ->1 c))') =< (a ^ b)''
22	21, 11	lbtr 139	. . . . . . . 8 ((a ^ b)'' ^ ((a ->1 c) ^ (b ->1 c))') =< (a ^ b)
23		leid 148	. . . . . . . 8 ((a ->1 c) ^ (b ->1 c)) =< ((a ->1 c) ^ (b ->1 c))
24	22, 23	le2or 168	. . . . . . 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 138	. . . . . 6 ((a ^ b)' ->2 ((a ->1 c) ^ (b ->1 c))) =< ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))
26	25, 16	letr 137	. . . . 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 158	. . . . . 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 35	. . . . . 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 139	. . . . 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 994	. . . 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 35	. . 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 771	. . . . . . 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 43	. . . . . . 7 ((a ^ b)' ->0 ((a ->1 c) ^ (b ->1 c))) = ((a ^ b)'' v ((a ->1 c) ^ (b ->1 c)))
34	32, 33	ax-r2 36	. . . . . 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 38	. . . . . . 7 ((a ^ b) v ((a ->1 c) ^ (b ->1 c))) = ((a ^ b)'' v ((a ->1 c) ^ (b ->1 c)))
36	35	ax-r1 35	. . . . . 6 ((a ^ b)'' v ((a ->1 c) ^ (b ->1 c))) = ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))
37	34, 36	ax-r2 36	. . . . 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