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

Theorem gomaex3 924
 Description: Proof of Mayet Example 3 from 6-variable Godowski equation. R. Mayet, "Equational bases for some varieties of orthomodular lattices related to states," Algebra Universalis 23 (1986), 167-195.
Hypotheses
Ref Expression
gomaex3.1
gomaex3.2
gomaex3.3
gomaex3.5
gomaex3.6
gomaex3.8
gomaex3.9
gomaex3.10
gomaex3.11
gomaex3.12
gomaex3.14
gomaex3.16
gomaex3.18
gomaex3.20
gomaex3.22
Assertion
Ref Expression
gomaex3

Proof of Theorem gomaex3
StepHypRef Expression
1 df-i1 44 . . . 4
2 ax-a2 31 . . . . . 6
3 gomaex3.9 . . . . . . . . . 10
43con2 67 . . . . . . . . 9
5 gomaex3.10 . . . . . . . . 9
64, 5ud1lem0ab 257 . . . . . . . 8
7 ax-a1 30 . . . . . . . 8
86, 7ax-r2 36 . . . . . . 7
9 gomaex3.11 . . . . . . . 8
106ax-r4 37 . . . . . . . . 9
1110ran 78 . . . . . . . 8
129, 11ax-r2 36 . . . . . . 7
138, 122or 72 . . . . . 6
142, 13ax-r2 36 . . . . 5
1514ax-r1 35 . . . 4
161, 15ax-r2 36 . . 3
1716lan 77 . 2
18 gomaex3.1 . . 3
19 gomaex3.2 . . 3
20 gomaex3.3 . . 3
21 gomaex3.5 . . 3
22 gomaex3.6 . . 3
23 gomaex3.8 . . 3
24 gomaex3.12 . . 3
25 id 59 . . 3
26 gomaex3.14 . . 3
27 id 59 . . 3
28 gomaex3.16 . . 3
29 id 59 . . 3
30 gomaex3.18 . . 3
31 id 59 . . 3
32 gomaex3.20 . . 3
33 id 59 . . 3
34 gomaex3.22 . . 3
35 id 59 . . 3
3618, 19, 20, 21, 22, 23, 3, 5, 9, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35gomaex3lem10 923 . 2
3717, 36bltr 138 1
 Colors of variables: term Syntax hints:   wb 1   wle 2  wn 4   wo 6   wa 7   wi1 12   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-i1 44  df-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133
 Copyright terms: Public domain W3C validator