Theorem go2n4 879

Description: 8-variable Godowski equation derived from 4-variable one. The last hypothesis is the 4-variable Godowski equation.

Hypotheses

Ref	Expression
go2n4.1	a =< b_|_
go2n4.2	b =< c_|_
go2n4.3	c =< d_|_
go2n4.4	d =< e_|_
go2n4.5	e =< f_|_
go2n4.6	f =< g_|_
go2n4.7	g =< h_|_
go2n4.8	h =< a_|_
go2n4.9	(((c ->2 a) ^ (a ->2 g)) ^ ((g ->2 e) ^ (e ->2 c))) =< (a ->2 c)

Assertion

Ref	Expression
go2n4	(((a v b) ^ (c v d)) ^ ((e v f) ^ (g v h))) =< (b v c)

Proof of Theorem go2n4

Step	Hyp	Ref	Expression
1		anass 69	. . 3 (((a v b) ^ (c v d)) ^ ((e v f) ^ (g v h))) = ((a v b) ^ ((c v d) ^ ((e v f) ^ (g v h))))
2		ancom 68	. . . 4 ((c v d) ^ ((e v f) ^ (g v h))) = (((e v f) ^ (g v h)) ^ (c v d))
3	2	lan 70	. . 3 ((a v b) ^ ((c v d) ^ ((e v f) ^ (g v h)))) = ((a v b) ^ (((e v f) ^ (g v h)) ^ (c v d)))
4	1, 3	ax-r2 35	. 2 (((a v b) ^ (c v d)) ^ ((e v f) ^ (g v h))) = ((a v b) ^ (((e v f) ^ (g v h)) ^ (c v d)))
5		go2n4.1	. . 3 a =< b_|_
6		go2n4.2	. . 3 b =< c_|_
7		anass 69	. . . . . 6 (((c ->2 a) ^ (a ->2 g)) ^ ((g ->2 e) ^ (e ->2 c))) = ((c ->2 a) ^ ((a ->2 g) ^ ((g ->2 e) ^ (e ->2 c))))
8		ancom 68	. . . . . . . 8 ((a ->2 g) ^ ((g ->2 e) ^ (e ->2 c))) = (((g ->2 e) ^ (e ->2 c)) ^ (a ->2 g))
9		an32 76	. . . . . . . 8 (((g ->2 e) ^ (e ->2 c)) ^ (a ->2 g)) = (((g ->2 e) ^ (a ->2 g)) ^ (e ->2 c))
10	8, 9	ax-r2 35	. . . . . . 7 ((a ->2 g) ^ ((g ->2 e) ^ (e ->2 c))) = (((g ->2 e) ^ (a ->2 g)) ^ (e ->2 c))
11	10	lan 70	. . . . . 6 ((c ->2 a) ^ ((a ->2 g) ^ ((g ->2 e) ^ (e ->2 c)))) = ((c ->2 a) ^ (((g ->2 e) ^ (a ->2 g)) ^ (e ->2 c)))
12	7, 11	ax-r2 35	. . . . 5 (((c ->2 a) ^ (a ->2 g)) ^ ((g ->2 e) ^ (e ->2 c))) = ((c ->2 a) ^ (((g ->2 e) ^ (a ->2 g)) ^ (e ->2 c)))
13	12	ax-r1 34	. . . 4 ((c ->2 a) ^ (((g ->2 e) ^ (a ->2 g)) ^ (e ->2 c))) = (((c ->2 a) ^ (a ->2 g)) ^ ((g ->2 e) ^ (e ->2 c)))
14		go2n4.9	. . . 4 (((c ->2 a) ^ (a ->2 g)) ^ ((g ->2 e) ^ (e ->2 c))) =< (a ->2 c)
15	13, 14	bltr 130	. . 3 ((c ->2 a) ^ (((g ->2 e) ^ (a ->2 g)) ^ (e ->2 c))) =< (a ->2 c)
16		go2n4.5	. . . . . 6 e =< f_|_
17		go2n4.6	. . . . . 6 f =< g_|_
18	16, 17	govar2 877	. . . . 5 (e v f) =< (g ->2 e)
19		go2n4.7	. . . . . 6 g =< h_|_
20		go2n4.8	. . . . . 6 h =< a_|_
21	19, 20	govar2 877	. . . . 5 (g v h) =< (a ->2 g)
22	18, 21	le2an 161	. . . 4 ((e v f) ^ (g v h)) =< ((g ->2 e) ^ (a ->2 g))
23		go2n4.3	. . . . 5 c =< d_|_
24		go2n4.4	. . . . 5 d =< e_|_
25	23, 24	govar2 877	. . . 4 (c v d) =< (e ->2 c)
26	22, 25	le2an 161	. . 3 (((e v f) ^ (g v h)) ^ (c v d)) =< (((g ->2 e) ^ (a ->2 g)) ^ (e ->2 c))
27	5, 6, 15, 26	gon2n 878	. 2 ((a v b) ^ (((e v f) ^ (g v h)) ^ (c v d))) =< (b v c)
28	4, 27	bltr 130	1 (((a v b) ^ (c v d)) ^ ((e v f) ^ (g v h))) =< (b v c)

Syntax hints:   =< wle 2  _|_wn 4   v wo 6   ^ wa 7   ->2 wi2 14

This theorem is referenced by:  gomaex4 880

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  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-i2 44  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org