Theorem List for Quantum Logic Explorer - 901-1000   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremgo2n6 901 12-variable Godowski equation derived from 6-variable one. The last hypothesis is the 6-variable Godowski equation. (Contributed by NM, 29-Nov-1999.)
gh    &   hi    &   ij    &   jk    &   km    &   mn    &   nu    &   uw    &   wx    &   xy    &   yz    &   zg    &   (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)       (((gh) ∩ (ij)) ∩ (((km) ∩ (nu)) ∩ ((wx) ∩ (yz)))) ≤ (hi)

Theoremgomaex3h1 902 Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
ab    &   g = a    &   h = b       gh

Theoremgomaex3h2 903 Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
bc    &   h = b    &   i = c       hi

Theoremgomaex3h3 904 Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
i = c    &   j = (cd)       ij

Theoremgomaex3h4 905 Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
r = ((p1 q) ∩ (cd))    &   j = (cd)    &   k = r       jk

Theoremgomaex3h5 906 Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
r = ((p1 q) ∩ (cd))    &   k = r    &   m = (p1 q)       km

Theoremgomaex3h6 907 Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
m = (p1 q)    &   n = (p1 q)       mn

Theoremgomaex3h7 908 Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
n = (p1 q)    &   u = (pq)       nu

Theoremgomaex3h8 909 Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
u = (pq)    &   w = q       uw

Theoremgomaex3h9 910 Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
w = q    &   x = q       wx

Theoremgomaex3h10 911 Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
q = ((ef) →1 (bc) )    &   x = q    &   y = (ef)       xy

Theoremgomaex3h11 912 Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
y = (ef)    &   z = f       yz

Theoremgomaex3h12 913 Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
fa    &   g = a    &   z = f       zg

Theoremgomaex3lem1 914 Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
cd       (c ∪ (cd) ) = d

Theoremgomaex3lem2 915 Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
ef       ((ef)f) = e

Theoremgomaex3lem3 916 Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
((p1 q) ∪ (pq)) = p

Theoremgomaex3lem4 917 Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
p = ((ab) →1 (de) )       ((ab) ∩ (de) ) ≤ p

Theoremgomaex3lem5 918 Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
ab    &   bc    &   cd    &   ef    &   fa    &   (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)    &   p = ((ab) →1 (de) )    &   q = ((ef) →1 (bc) )    &   r = ((p1 q) ∩ (cd))    &   g = a    &   h = b    &   i = c    &   j = (cd)    &   k = r    &   m = (p1 q)    &   n = (p1 q)    &   u = (pq)    &   w = q    &   x = q    &   y = (ef)    &   z = f       (((gh) ∩ (ij)) ∩ (((km) ∩ (nu)) ∩ ((wx) ∩ (yz)))) ≤ (hi)

Theoremgomaex3lem6 919 Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
ab    &   bc    &   cd    &   ef    &   fa    &   (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)    &   p = ((ab) →1 (de) )    &   q = ((ef) →1 (bc) )    &   r = ((p1 q) ∩ (cd))    &   g = a    &   h = b    &   i = c    &   j = (cd)    &   k = r    &   m = (p1 q)    &   n = (p1 q)    &   u = (pq)    &   w = q    &   x = q    &   y = (ef)    &   z = f       (((ab) ∩ (c ∪ (cd) )) ∩ (((r ∪ (p1 q)) ∩ ((p1 q) ∪ (pq))) ∩ ((qq) ∩ ((ef)f)))) ≤ (bc)

Theoremgomaex3lem7 920 Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
ab    &   bc    &   cd    &   ef    &   fa    &   (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)    &   p = ((ab) →1 (de) )    &   q = ((ef) →1 (bc) )    &   r = ((p1 q) ∩ (cd))    &   g = a    &   h = b    &   i = c    &   j = (cd)    &   k = r    &   m = (p1 q)    &   n = (p1 q)    &   u = (pq)    &   w = q    &   x = q    &   y = (ef)    &   z = f       (((ab) ∩ d ) ∩ (((r ∪ (p1 q)) ∩ p ) ∩ e )) ≤ (bc)

Theoremgomaex3lem8 921 Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
ab    &   bc    &   cd    &   ef    &   fa    &   (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)    &   p = ((ab) →1 (de) )    &   q = ((ef) →1 (bc) )    &   r = ((p1 q) ∩ (cd))    &   g = a    &   h = b    &   i = c    &   j = (cd)    &   k = r    &   m = (p1 q)    &   n = (p1 q)    &   u = (pq)    &   w = q    &   x = q    &   y = (ef)    &   z = f       (((ab) ∩ (de) ) ∩ ((r ∪ (p1 q)) ∩ p )) ≤ (bc)

Theoremgomaex3lem9 922 Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
ab    &   bc    &   cd    &   ef    &   fa    &   (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)    &   p = ((ab) →1 (de) )    &   q = ((ef) →1 (bc) )    &   r = ((p1 q) ∩ (cd))    &   g = a    &   h = b    &   i = c    &   j = (cd)    &   k = r    &   m = (p1 q)    &   n = (p1 q)    &   u = (pq)    &   w = q    &   x = q    &   y = (ef)    &   z = f       (((ab) ∩ (de) ) ∩ (r ∪ (p1 q))) ≤ (bc)

Theoremgomaex3lem10 923 Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
ab    &   bc    &   cd    &   ef    &   fa    &   (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)    &   p = ((ab) →1 (de) )    &   q = ((ef) →1 (bc) )    &   r = ((p1 q) ∩ (cd))    &   g = a    &   h = b    &   i = c    &   j = (cd)    &   k = r    &   m = (p1 q)    &   n = (p1 q)    &   u = (pq)    &   w = q    &   x = q    &   y = (ef)    &   z = f       (((ab) ∩ (de) ) ∩ (r ∪ (p1 q))) ≤ ((bc) ∪ (ef) )

Theoremgomaex3 924 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. (Contributed by NM, 27-May-2000.)
ab    &   bc    &   cd    &   ef    &   fa    &   (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)    &   p = ((ab) →1 (de) )    &   q = ((ef) →1 (bc) )    &   r = ((p1 q) ∩ (cd))    &   g = a    &   i = c    &   k = r    &   n = (p1 q)    &   w = q    &   y = (ef)       (((ab) ∩ (de) ) ∩ ((((ab) →1 (de) ) →1 ((ef) →1 (bc) ) )1 (cd))) ≤ ((bc) ∪ (ef) )

0.3.11  OML lemmas for studying orthoarguesian laws

Theoremoas 925 "Strengthening" lemma for studying the orthoarguesian law. (Contributed by NM, 25-Dec-1998.)
(a ∩ (ab)) ≤ c       ((a1 c) ∩ (ab)) ≤ c

Theoremoasr 926 Reverse of oas 925 lemma for studying the orthoarguesian law. (Contributed by NM, 28-Dec-1998.)
((a1 c) ∩ (ab)) ≤ c       (a ∩ (ab)) ≤ c

Theoremoat 927 Transformation lemma for studying the orthoarguesian law. (Contributed by NM, 26-Dec-1998.)
(a ∩ (ab)) ≤ c       b ≤ (a1 c)

Theoremoatr 928 Reverse transformation lemma for studying the orthoarguesian law. (Contributed by NM, 26-Dec-1998.)
b ≤ (a1 c)       (a ∩ (ab)) ≤ c

Theoremoau 929 Transformation lemma for studying the orthoarguesian law. (Contributed by NM, 28-Dec-1998.)
(a ∩ ((a1 c) ∪ b)) ≤ c       b ≤ (a1 c)

Theoremoaur 930 Transformation lemma for studying the orthoarguesian law. (Contributed by NM, 28-Dec-1998.)
b ≤ (a1 c)       (a ∩ ((a1 c) ∪ b)) ≤ c

Theoremoaidlem2 931 Lemma for identity-like OA law. (Contributed by NM, 22-Jan-1999.)
((d ∪ ((a1 c) ∩ (b1 c))) ∪ ((a1 c) →1 (b1 c))) = 1       ((a1 c) ∩ (d ∪ ((a1 c) ∩ (b1 c)))) ≤ (b1 c)

Theoremoaidlem2g 932 Lemma for identity-like OA law (generalized). (Contributed by NM, 18-Feb-2002.)
((c ∪ (ab)) ∪ (a1 b)) = 1       (a ∩ (c ∪ (ab))) ≤ b

Theoremoa6v4v 933 6-variable OA to 4-variable OA. (Contributed by NM, 29-Nov-1998.)
(((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))    &   e = 0    &   f = 1       ((ab) ∩ (cd)) ≤ (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))

Theoremoa4v3v 934 4-variable OA to 3-variable OA (Godowski/Greechie Eq. IV). (Contributed by NM, 28-Nov-1998.)
db    &   ec    &   ((db) ∩ (ec)) ≤ (b ∪ (d ∩ (e ∪ ((de) ∩ (bc)))))    &   d = (a2 b)    &   e = (a2 c)       (b ∩ ((a2 b) ∪ ((a2 c) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))))) ≤ ((b ∩ (a2 b)) ∪ (c ∩ (a2 c)))

Theoremoal42 935 Derivation of Godowski/Greechie Eq. II from Eq. IV. (Contributed by NM, 25-Nov-1998.)
(b ∩ ((a2 b) ∪ ((a2 c) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))))) ≤ ((b ∩ (a2 b)) ∪ (c ∩ (a2 c)))       (b ∩ ((a2 b) ∪ ((a2 c) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))))) ≤ a

Theoremoa23 936 Derivation of OA from Godowski/Greechie Eq. II. (Contributed by NM, 25-Nov-1998.)
(c ∩ ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))) ≤ a       ((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ≤ (a2 c)

Theoremoa4lem1 937 Lemma for 3-var to 4-var OA. (Contributed by NM, 27-Nov-1998.)
ab    &   cd       (ab) ≤ ((ac)2 b)

Theoremoa4lem2 938 Lemma for 3-var to 4-var OA. (Contributed by NM, 27-Nov-1998.)
ab    &   cd       (cd) ≤ ((ac)2 d)

Theoremoa4lem3 939 Lemma for 3-var to 4-var OA. (Contributed by NM, 27-Nov-1998.)
ab    &   cd       ((ab) ∩ (cd)) ≤ ((bd) ∪ (((ac)2 b) ∩ ((ac)2 d)))

Theoremdistoah1 940 Satisfaction of distributive law hypothesis. (Contributed by NM, 29-Nov-1998.)
d = (a2 b)    &   e = ((bc) →1 ((a2 b) ∩ (a2 c)))    &   f = ((bc) →2 ((a2 b) ∩ (a2 c)))       d ≤ (a2 b)

Theoremdistoah2 941 Satisfaction of distributive law hypothesis. (Contributed by NM, 29-Nov-1998.)
d = (a2 b)    &   e = ((bc) →1 ((a2 b) ∩ (a2 c)))    &   f = ((bc) →2 ((a2 b) ∩ (a2 c)))       e ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))

Theoremdistoah3 942 Satisfaction of distributive law hypothesis. (Contributed by NM, 29-Nov-1998.)
d = (a2 b)    &   e = ((bc) →1 ((a2 b) ∩ (a2 c)))    &   f = ((bc) →2 ((a2 b) ∩ (a2 c)))       f ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))

Theoremdistoah4 943 Satisfaction of distributive law hypothesis. (Contributed by NM, 29-Nov-1998.)
d = (a2 b)    &   e = ((bc) →1 ((a2 b) ∩ (a2 c)))    &   f = ((bc) →2 ((a2 b) ∩ (a2 c)))       (d ∩ (a2 c)) ≤ f

Theoremdistoa 944 Derivation in OM of OA, assuming OA distributive law oadistd 1023. (Contributed by NM, 29-Nov-1998.)
d = (a2 b)    &   e = ((bc) →1 ((a2 b) ∩ (a2 c)))    &   f = ((bc) →2 ((a2 b) ∩ (a2 c)))    &   (d ∩ (ef)) = ((de) ∪ (df))       ((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ≤ (a2 c)

Theoremoa3to4lem1 945 Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof). (Contributed by NM, 19-Dec-1998.)
ab    &   cd    &   g = ((ab) ∪ (cd))       b ≤ (a1 g)

Theoremoa3to4lem2 946 Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof). (Contributed by NM, 19-Dec-1998.)
ab    &   cd    &   g = ((ab) ∪ (cd))       d ≤ (c1 g)

Theoremoa3to4lem3 947 Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof). (Contributed by NM, 19-Dec-1998.)
ab    &   cd    &   g = ((ab) ∪ (cd))       (a ∩ (b ∪ (d ∩ ((ac) ∪ (bd))))) ≤ (a ∩ ((a1 g) ∪ ((c1 g) ∩ ((ac) ∪ ((a1 g) ∩ (c1 g))))))

Theoremoa3to4lem4 948 Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof). (Contributed by NM, 19-Dec-1998.)
ab    &   cd    &   g = ((ab) ∪ (cd))    &   (a ∩ ((a1 g) ∪ ((c1 g) ∩ ((ac) ∪ ((a1 g) ∩ (c1 g)))))) ≤ ((ag) ∪ (cg))       (a ∩ (b ∪ (d ∩ ((ac) ∪ (bd))))) ≤ g

Theoremoa3to4lem5 949 Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof). (Contributed by NM, 19-Dec-1998.)
((ab) ∩ (cd)) ≤ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))       ((ba) ∩ (dc)) ≤ (a ∪ (b ∩ (d ∪ ((bd) ∩ (ac)))))

Theoremoa3to4lem6 950 Orthoarguesian law (Godowski/Greechie 3-variable to 4-variable). The first 2 hypotheses are those for 4-OA. The next 3 are variable substitutions into 3-OA. The last is the 3-OA. The proof uses OM logic only. (Contributed by NM, 19-Dec-1998.)
ab    &   cd    &   g = ((ab ) ∪ (cd ))    &   e = a    &   f = c    &   (e ∩ ((e1 g) ∪ ((f1 g) ∩ ((ef) ∪ ((e1 g) ∩ (f1 g)))))) ≤ ((eg) ∪ (fg))       ((ab) ∩ (cd)) ≤ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))

Theoremoa3to4 951 Orthoarguesian law (Godowski/Greechie 3-variable to 4-variable). The first 2 hypotheses are those for 4-OA. The next 3 are variable substitutions into 3-OA. The last is the 3-OA. The proof uses OM logic only. (Contributed by NM, 19-Dec-1998.)
ab    &   cd    &   g = ((ba ) ∪ (dc ))    &   e = b    &   f = d    &   (e ∩ ((e1 g) ∪ ((f1 g) ∩ ((ef) ∪ ((e1 g) ∩ (f1 g)))))) ≤ ((eg) ∪ (fg))       ((ab) ∩ (cd)) ≤ (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))

Theoremoa6todual 952 Conventional to dual 6-variable OA law. (Contributed by NM, 22-Dec-1998.)
(((ab ) ∩ (cd )) ∩ (ef )) ≤ (b ∪ (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))))))       (b ∩ (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))))) ≤ (((ab) ∪ (cd)) ∪ (ef))

Theoremoa6fromdual 953 Dual to conventional 6-variable OA law. (Contributed by NM, 22-Dec-1998.)
(b ∩ (a ∪ (c ∩ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df ))))))) ≤ (((ab ) ∪ (cd )) ∪ (ef ))       (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))

Theoremoa6fromdualn 954 Dual to conventional 6-variable OA law. (Contributed by NM, 24-Dec-1998.)
(b ∩ (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))))) ≤ (((ab) ∪ (cd)) ∪ (ef))       (((ab ) ∩ (cd )) ∩ (ef )) ≤ (b ∪ (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))))))

Theoremoa6to4h1 955 Satisfaction of 6-variable OA law hypothesis. (Contributed by NM, 22-Dec-1998.)
b = (a1 g)    &   d = (c1 g)    &   f = (e1 g)       ab

Theoremoa6to4h2 956 Satisfaction of 6-variable OA law hypothesis. (Contributed by NM, 22-Dec-1998.)
b = (a1 g)    &   d = (c1 g)    &   f = (e1 g)       cd

Theoremoa6to4h3 957 Satisfaction of 6-variable OA law hypothesis. (Contributed by NM, 22-Dec-1998.)
b = (a1 g)    &   d = (c1 g)    &   f = (e1 g)       ef

Theoremoa6to4 958 Derivation of 4-variable proper OA law, assuming 6-variable OA law. (Contributed by NM, 22-Dec-1998.)
b = (a1 g)    &   d = (c1 g)    &   f = (e1 g)    &   (((ab ) ∩ (cd )) ∩ (ef )) ≤ (b ∪ (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))))))       ((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ (((ag) ∪ (cg)) ∪ (eg))

Theoremoa4b 959 Derivation of 4-OA law variant. (Contributed by NM, 22-Dec-1998.)
((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ (((ag) ∪ (cg)) ∪ (eg))       ((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ g

Theoremoa4to6lem1 960 Lemma for orthoarguesian law (4-variable to 6-variable proof). (Contributed by NM, 18-Dec-1998.)
ab    &   cd    &   ef    &   g = (((ab) ∪ (cd)) ∪ (ef))       b ≤ (a1 g)

Theoremoa4to6lem2 961 Lemma for orthoarguesian law (4-variable to 6-variable proof). (Contributed by NM, 18-Dec-1998.)
ab    &   cd    &   ef    &   g = (((ab) ∪ (cd)) ∪ (ef))       d ≤ (c1 g)

Theoremoa4to6lem3 962 Lemma for orthoarguesian law (4-variable to 6-variable proof). (Contributed by NM, 18-Dec-1998.)
ab    &   cd    &   ef    &   g = (((ab) ∪ (cd)) ∪ (ef))       f ≤ (e1 g)

Theoremoa4to6lem4 963 Lemma for orthoarguesian law (4-variable to 6-variable proof). (Contributed by NM, 18-Dec-1998.)
ab    &   cd    &   ef    &   g = (((ab) ∪ (cd)) ∪ (ef))       (b ∩ (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))))) ≤ ((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g))))))))

Theoremoa4to6dual 964 Lemma for orthoarguesian law (4-variable to 6-variable proof). (Contributed by NM, 19-Dec-1998.)
ab    &   cd    &   ef    &   g = (((ab) ∪ (cd)) ∪ (ef))    &   ((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ g       (b ∩ (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))))) ≤ g

Theoremoa4to6 965 Orthoarguesian law (4-variable to 6-variable proof). The first 3 hypotheses are those for 6-OA. The next 4 are variable substitutions into 4-OA. The last is the 4-OA. The proof uses OM logic only. (Contributed by NM, 19-Dec-1998.)
ab    &   cd    &   ef    &   g = (((ab ) ∪ (cd )) ∪ (ef ))    &   h = a    &   j = c    &   k = e    &   ((h1 g) ∩ (h ∪ (j ∩ (((hj) ∪ ((h1 g) ∩ (j1 g))) ∪ (((hk) ∪ ((h1 g) ∩ (k1 g))) ∩ ((jk) ∪ ((j1 g) ∩ (k1 g)))))))) ≤ g       (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))

Theoremoa4btoc 966 Derivation of 4-OA law variant. (Contributed by NM, 22-Dec-1998.)
((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ g       (a ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ g

Theoremoa4ctob 967 Derivation of 4-OA law variant. (Contributed by NM, 22-Dec-1998.)
(a ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ g       ((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ g

Theoremoa4ctod 968 Derivation of 4-OA law variant. (Contributed by NM, 24-Dec-1998.)
(a ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d       (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))) ≤ (a1 d)

Theoremoa4dtoc 969 Derivation of 4-OA law variant. (Contributed by NM, 24-Dec-1998.)
(b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))) ≤ (a1 d)       (a ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d

Theoremoa4dcom 970 Lemma commuting terms. (Contributed by NM, 24-Dec-1998.)
(b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))) = (b ∩ (((ba) ∪ ((b1 d) ∩ (a1 d))) ∪ (((bc) ∪ ((b1 d) ∩ (c1 d))) ∩ ((ac) ∪ ((a1 d) ∩ (c1 d))))))

0.3.12  5OA law

Theoremoa8todual 971 Conventional to dual 8-variable OA law. (Contributed by NM, 8-May-2000.)
(((ab ) ∩ (cd )) ∩ ((ef ) ∩ (gh ))) ≤ (b ∪ (a ∩ (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))))))))       (b ∩ (a ∪ (c ∩ ((((ac) ∪ (bd)) ∪ (((ag) ∪ (bh)) ∩ ((cg) ∪ (dh)))) ∪ ((((ae) ∪ (bf)) ∪ (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh)))) ∩ (((ce) ∪ (df)) ∪ (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh))))))))) ≤ (((ab) ∪ (cd)) ∪ ((ef) ∪ (gh)))

Theoremoa8to5 972 Orthoarguesian law 5OA converted from 8 to 5 variables. (Contributed by NM, 8-May-2000.)
(((ab ) ∩ (cd )) ∩ ((ef ) ∩ (gh ))) ≤ (b ∪ (a ∩ (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))))))))    &   b = (a1 j)    &   d = (c1 j)    &   f = (e1 j)    &   h = (g1 j)       ((a1 j) ∩ (a ∪ (c ∩ ((((ac) ∪ ((a1 j) ∩ (c1 j))) ∪ (((ag) ∪ ((a1 j) ∩ (g1 j))) ∩ ((cg) ∪ ((c1 j) ∩ (g1 j))))) ∪ ((((ae) ∪ ((a1 j) ∩ (e1 j))) ∪ (((ag) ∪ ((a1 j) ∩ (g1 j))) ∩ ((eg) ∪ ((e1 j) ∩ (g1 j))))) ∩ (((ce) ∪ ((c1 j) ∩ (e1 j))) ∪ (((cg) ∪ ((c1 j) ∩ (g1 j))) ∩ ((eg) ∪ ((e1 j) ∩ (g1 j)))))))))) ≤ (((aj) ∪ (cj)) ∪ ((ej) ∪ (gj)))

0.3.13  "Godowski/Greechie" form of proper 4-OA

Theoremoa4to4u 973 A "universal" 4-OA. The hypotheses are the standard proper 4-OA and substitutions into it. (Contributed by NM, 28-Dec-1998.)
((e1 d) ∩ (e ∪ (f ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))))))) ≤ (((ed) ∪ (fd)) ∪ (gd))    &   e = (a1 d)    &   f = (b1 d)    &   g = (c1 d)       ((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ ((((a1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (b1 d))) ∪ ((c1 d) ∩ (c1 d)))

Theoremoa4to4u2 974 A weaker-looking "universal" proper 4-OA. (Contributed by NM, 29-Dec-1998.)
((e1 d) ∩ (e ∪ (f ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))))))) ≤ (((ed) ∪ (fd)) ∪ (gd))    &   e = (a1 d)    &   f = (b1 d)    &   g = (c1 d)       ((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d

Theoremoa4uto4g 975 Derivation of "Godowski/Greechie" 4-variable proper OA law variant from "universal" variant oa4to4u2 974. (Contributed by NM, 28-Dec-1998.)
((b1 d) ∩ ((b 1 d) ∪ ((a 1 d) ∩ ((((b1 d) ∩ (a1 d)) ∪ ((b 1 d) ∩ (a 1 d))) ∪ ((((b1 d) ∩ (c1 d)) ∪ ((b 1 d) ∩ (c 1 d))) ∩ (((a1 d) ∩ (c1 d)) ∪ ((a 1 d) ∩ (c 1 d)))))))) ≤ d    &   h = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))       ((a1 d) ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ h)) ≤ (b1 d)

Theoremoa4gto4u 976 A "universal" 4-OA derived from the Godowski/Greechie form. The hypotheses are the Godowski/Greechie form of the proper 4-OA and substitutions into it. (Contributed by NM, 30-Dec-1998.)
((e1 d) ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))))) ≤ (f1 d)    &   f = (a1 d)    &   e = (b1 d)    &   g = (c1 d)       ((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d

Theoremoa4uto4 977 Derivation of standard 4-variable proper OA law from "universal" variant oa4to4u2 974. (Contributed by NM, 30-Dec-1998.)
((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d       ((a1 d) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d

0.3.14  Some 3-OA inferences (derived under OM)

Theoremoa3-2lema 978 Lemma for 3-OA(2). Equivalence with substitution into 4-OA. (Contributed by NM, 24-Dec-1998.)
((a1 c) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 c) ∩ (b1 c))) ∪ (((a ∩ 0) ∪ ((a1 c) ∩ (0 →1 c))) ∩ ((b ∩ 0) ∪ ((b1 c) ∩ (0 →1 c)))))))) = ((a1 c) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))

Theoremoa3-2lemb 979 Lemma for 3-OA(2). Equivalence with substitution into 4-OA. (Contributed by NM, 24-Dec-1998.)
((a1 c) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 c) ∩ (b1 c))) ∪ (((ac) ∪ ((a1 c) ∩ (c1 c))) ∩ ((bc) ∪ ((b1 c) ∩ (c1 c)))))))) = ((a1 c) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))

Theoremoa3-6lem 980 Lemma for 3-OA(6). Equivalence with substitution into 4-OA. (Contributed by NM, 24-Dec-1998.)
((a1 c) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 c) ∩ (b1 c))) ∪ (((a ∩ 1) ∪ ((a1 c) ∩ (1 →1 c))) ∩ ((b ∩ 1) ∪ ((b1 c) ∩ (1 →1 c)))))))) = ((a1 c) ∩ (a ∪ (b ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))))

Theoremoa3-3lem 981 Lemma for 3-OA(3). Equivalence with substitution into 6-OA dual. (Contributed by NM, 24-Dec-1998.)
(a ∩ (a ∪ (b ∩ (((ab) ∪ (ab )) ∪ (((a ∩ 1) ∪ (ac)) ∩ ((b ∩ 1) ∪ (bc))))))) = (a ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))

Theoremoa3-1lem 982 Lemma for 3-OA(1). Equivalence with substitution into 6-OA dual. (Contributed by NM, 25-Dec-1998.)
(1 ∩ (0 ∪ (a ∩ (((0 ∩ a) ∪ (1 ∩ (a1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))))) = (a ∩ ((a1 c) ∪ ((b1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))

Theoremoa3-4lem 983 Lemma for 3-OA(4). Equivalence with substitution into 6-OA dual. (Contributed by NM, 25-Dec-1998.)
(a ∩ (a ∪ (b ∩ (((ab) ∪ (ab )) ∪ (((ac) ∪ (a ∩ 1)) ∩ ((bc) ∪ (b ∩ 1))))))) = (a ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))

Theoremoa3-5lem 984 Lemma for 3-OA(5). Equivalence with substitution into 6-OA dual. (Contributed by NM, 25-Dec-1998.)
((a1 c) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 c) ∩ 1)) ∪ (((ab) ∪ ((a1 c) ∩ (b1 c))) ∩ ((cb) ∪ (1 ∩ (b1 c)))))))) = ((a1 c) ∩ (a ∪ (c ∩ ((a1 c) ∪ ((b1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))))

Theoremoa3-u1lem 985 Lemma for a "universal" 3-OA. Equivalence with substitution into 6-OA dual. (Contributed by NM, 26-Dec-1998.)
(1 ∩ (c ∪ ((a1 c) ∩ (((c ∩ (a1 c)) ∪ (1 ∩ (a1 c))) ∪ (((c ∩ (b1 c)) ∪ (1 ∩ (b1 c))) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))))))) = (c ∪ ((a1 c) ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))))))

Theoremoa3-u2lem 986 Lemma for a "universal" 3-OA. Equivalence with substitution into 6-OA dual. (Contributed by NM, 27-Dec-1998.)
((a1 c) ∩ ((a1 c) ∪ (c ∩ ((((a1 c) ∩ c) ∪ ((a1 c) ∩ 1)) ∪ ((((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))) ∩ ((c ∩ (b1 c)) ∪ (1 ∩ (b1 c)))))))) = ((a1 c) ∩ ((a1 c) ∪ (c ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))))))

Theoremoa3-6to3 987 Derivation of 3-OA variant (3) from (6). (Contributed by NM, 24-Dec-1998.)
((a1 c) ∩ (a ∪ (b ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))))) ≤ c       (a ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ≤ c

Theoremoa3-2to4 988 Derivation of 3-OA variant (4) from (2). (Contributed by NM, 24-Dec-1998.)
((a1 c) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ≤ c       (a ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ≤ c

Theoremoa3-2wto2 989 Derivation of 3-OA variant from weaker version. (Contributed by NM, 25-Dec-1998.)
(a ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ≤ c       ((a1 c) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ≤ c

Theoremoa3-2to2s 990 Derivation of 3-OA variant from weaker version. (Contributed by NM, 25-Dec-1998.)
((a1 d) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 d) ∩ (b1 d)))))) ≤ d    &   d = ((ac) ∪ (bc))       ((a1 c) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ≤ ((ac) ∪ (bc))

Theoremoa3-u1 991 Derivation of a "universal" 3-OA. The hypothesis is a substitution instance of the proper 4-OA. (Contributed by NM, 27-Dec-1998.)
((c1 c) ∩ (c ∪ ((a1 c) ∩ (((c ∩ (a1 c)) ∪ ((c1 c) ∩ ((a1 c) →1 c))) ∪ (((c ∩ (b1 c)) ∪ ((c1 c) ∩ ((b1 c) →1 c))) ∩ (((a1 c) ∩ (b1 c)) ∪ (((a1 c) →1 c) ∩ ((b1 c) →1 c)))))))) ≤ c       (c ∪ ((a1 c) ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))))) ≤ c

Theoremoa3-u2 992 Derivation of a "universal" 3-OA. The hypothesis is a substitution instance of the proper 4-OA. (Contributed by NM, 27-Dec-1998.)
(((a1 c) →1 c) ∩ ((a1 c) ∪ (c ∩ ((((a1 c) ∩ c) ∪ (((a1 c) →1 c) ∩ (c1 c))) ∪ ((((a1 c) ∩ (b1 c)) ∪ (((a1 c) →1 c) ∩ ((b1 c) →1 c))) ∩ ((c ∩ (b1 c)) ∪ ((c1 c) ∩ ((b1 c) →1 c)))))))) ≤ c       ((a1 c) ∩ ((a1 c) ∪ (c ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))))))) ≤ c

Theoremoa3-1to5 993 Derivation of an equivalent of the second "universal" 3-OA U2 from an equivalent of the first "universal" 3-OA U1. This shows that U2 is redundant in a system containg U1. The hypothesis is theorem oal1 1000. (Contributed by NM, 1-Jan-1999.)
((a1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))) ≤ (b1 c)       (c ∩ ((b1 c) ∪ ((a1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ≤ (b1 c)

0.4  Derivation of 4-variable proper OA from OA distributive law

In this section, we postulate a temporary axiom (intended not to be used outside of this section) for the OA distributive law, and derive from it the proper 4-OA. This shows that the OA distributive law implies the proper 4-OA (and therefore the 6-OA).

Axiomax-oadist 994 OA Distributive law. In this section, we postulate this temporary axiom (intended not to be used outside of this section) for the OA distributive law, and derive from it the 6-OA, in theorem d6oa 997. This together with the derivation of the distributive law in theorem 4oadist 1044 shows that the OA distributive law is equivalent to the 6-OA. (Contributed by NM, 30-Dec-1998.)
e = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))    &   f = (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ e)    &   h ≤ (a1 d)    &   jf    &   kf    &   (h ∩ (b1 d)) ≤ k       (h ∩ (jk)) = ((hj) ∪ (hk))

Theoremd3oa 995 Derivation of 3-OA from OA distributive law. (Contributed by NM, 30-Dec-1998.)
f = ((ab) ∪ ((a1 c) ∩ (b1 c)))       ((a1 c) ∩ f) ≤ (b1 c)

Theoremd4oa 996 Variant of proper 4-OA proved from OA distributive law. (Contributed by NM, 30-Dec-1998.)
e = ((ab) ∪ ((a1 d) ∩ (b1 d)))    &   f = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))       ((a1 d) ∩ (ef)) ≤ (b1 d)

Theoremd6oa 997 Derivation of 6-variable orthoarguesian law from OA distributive law. (Contributed by NM, 30-Dec-1998.)
ab    &   cd    &   ef       (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))

0.5  Orthoarguesian laws

R. Godowski and R. Greechie, Demonstratio Mathematica 17, 241 (1984).

0.5.1  3-variable orthoarguesian law

Axiomax-3oa 998 3-variable consequence of the orthoarguesion law. (Contributed by NM, 20-Jul-1999.)
((a1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))) ≤ (b1 c)

Theoremoal2 999 Orthoarguesian law - 2 version. (Contributed by NM, 20-Jul-1999.)
((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ≤ (a2 c)

Theoremoal1 1000 Orthoarguesian law - 1 version derived from 1 version. (Contributed by NM, 25-Nov-1998.)
((a1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))) ≤ (b1 c)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1217
 Copyright terms: Public domain < Previous  Next >