Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  go2n4 GIF version

Theorem go2n4 899
 Description: 8-variable Godowski equation derived from 4-variable one. The last hypothesis is the 4-variable Godowski equation.
Hypotheses
Ref Expression
go2n4.1 ab
go2n4.2 bc
go2n4.3 cd
go2n4.4 de
go2n4.5 ef
go2n4.6 fg
go2n4.7 gh
go2n4.8 ha
go2n4.9 (((c2 a) ∩ (a2 g)) ∩ ((g2 e) ∩ (e2 c))) ≤ (a2 c)
Assertion
Ref Expression
go2n4 (((ab) ∩ (cd)) ∩ ((ef) ∩ (gh))) ≤ (bc)

Proof of Theorem go2n4
StepHypRef Expression
1 anass 76 . . 3 (((ab) ∩ (cd)) ∩ ((ef) ∩ (gh))) = ((ab) ∩ ((cd) ∩ ((ef) ∩ (gh))))
2 ancom 74 . . . 4 ((cd) ∩ ((ef) ∩ (gh))) = (((ef) ∩ (gh)) ∩ (cd))
32lan 77 . . 3 ((ab) ∩ ((cd) ∩ ((ef) ∩ (gh)))) = ((ab) ∩ (((ef) ∩ (gh)) ∩ (cd)))
41, 3ax-r2 36 . 2 (((ab) ∩ (cd)) ∩ ((ef) ∩ (gh))) = ((ab) ∩ (((ef) ∩ (gh)) ∩ (cd)))
5 go2n4.1 . . 3 ab
6 go2n4.2 . . 3 bc
7 anass 76 . . . . . 6 (((c2 a) ∩ (a2 g)) ∩ ((g2 e) ∩ (e2 c))) = ((c2 a) ∩ ((a2 g) ∩ ((g2 e) ∩ (e2 c))))
8 ancom 74 . . . . . . . 8 ((a2 g) ∩ ((g2 e) ∩ (e2 c))) = (((g2 e) ∩ (e2 c)) ∩ (a2 g))
9 an32 83 . . . . . . . 8 (((g2 e) ∩ (e2 c)) ∩ (a2 g)) = (((g2 e) ∩ (a2 g)) ∩ (e2 c))
108, 9ax-r2 36 . . . . . . 7 ((a2 g) ∩ ((g2 e) ∩ (e2 c))) = (((g2 e) ∩ (a2 g)) ∩ (e2 c))
1110lan 77 . . . . . 6 ((c2 a) ∩ ((a2 g) ∩ ((g2 e) ∩ (e2 c)))) = ((c2 a) ∩ (((g2 e) ∩ (a2 g)) ∩ (e2 c)))
127, 11ax-r2 36 . . . . 5 (((c2 a) ∩ (a2 g)) ∩ ((g2 e) ∩ (e2 c))) = ((c2 a) ∩ (((g2 e) ∩ (a2 g)) ∩ (e2 c)))
1312ax-r1 35 . . . 4 ((c2 a) ∩ (((g2 e) ∩ (a2 g)) ∩ (e2 c))) = (((c2 a) ∩ (a2 g)) ∩ ((g2 e) ∩ (e2 c)))
14 go2n4.9 . . . 4 (((c2 a) ∩ (a2 g)) ∩ ((g2 e) ∩ (e2 c))) ≤ (a2 c)
1513, 14bltr 138 . . 3 ((c2 a) ∩ (((g2 e) ∩ (a2 g)) ∩ (e2 c))) ≤ (a2 c)
16 go2n4.5 . . . . . 6 ef
17 go2n4.6 . . . . . 6 fg
1816, 17govar2 897 . . . . 5 (ef) ≤ (g2 e)
19 go2n4.7 . . . . . 6 gh
20 go2n4.8 . . . . . 6 ha
2119, 20govar2 897 . . . . 5 (gh) ≤ (a2 g)
2218, 21le2an 169 . . . 4 ((ef) ∩ (gh)) ≤ ((g2 e) ∩ (a2 g))
23 go2n4.3 . . . . 5 cd
24 go2n4.4 . . . . 5 de
2523, 24govar2 897 . . . 4 (cd) ≤ (e2 c)
2622, 25le2an 169 . . 3 (((ef) ∩ (gh)) ∩ (cd)) ≤ (((g2 e) ∩ (a2 g)) ∩ (e2 c))
275, 6, 15, 26gon2n 898 . 2 ((ab) ∩ (((ef) ∩ (gh)) ∩ (cd))) ≤ (bc)
284, 27bltr 138 1 (((ab) ∩ (cd)) ∩ ((ef) ∩ (gh))) ≤ (bc)
 Colors of variables: term Syntax hints:   ≤ wle 2  ⊥ wn 4   ∪ wo 6   ∩ wa 7   →2 wi2 13 This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439 This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133 This theorem is referenced by:  gomaex4  900
 Copyright terms: Public domain W3C validator