P. 10 of Theorem List - Quantum Logic Explorer

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

Type	Label	Description
Statement
Theorem	go2n6 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.)
g ≤ h⊥    &   h ≤ i⊥    &   i ≤ j⊥    &   j ≤ k⊥    &   k ≤ m⊥    &   m ≤ n⊥    &   n ≤ u⊥    &   u ≤ w⊥    &   w ≤ x⊥    &   x ≤ y⊥    &   y ≤ z⊥    &   z ≤ g⊥    &   (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)    ⇒   (((g ∪ h) ∩ (i ∪ j)) ∩ (((k ∪ m) ∩ (n ∪ u)) ∩ ((w ∪ x) ∩ (y ∪ z)))) ≤ (h ∪ i)
Theorem	gomaex3h1 902	Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
a ≤ b⊥    &   g = a    &   h = b    ⇒   g ≤ h⊥
Theorem	gomaex3h2 903	Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
b ≤ c⊥    &   h = b    &   i = c    ⇒   h ≤ i⊥
Theorem	gomaex3h3 904	Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
i = c    &   j = (c ∪ d)⊥    ⇒   i ≤ j⊥
Theorem	gomaex3h4 905	Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))    &   j = (c ∪ d)⊥    &   k = r    ⇒   j ≤ k⊥
Theorem	gomaex3h5 906	Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))    &   k = r    &   m = (p⊥ →1 q)    ⇒   k ≤ m⊥
Theorem	gomaex3h6 907	Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
m = (p⊥ →1 q)    &   n = (p⊥ →1 q)⊥    ⇒   m ≤ n⊥
Theorem	gomaex3h7 908	Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
n = (p⊥ →1 q)⊥    &   u = (p⊥ ∩ q)    ⇒   n ≤ u⊥
Theorem	gomaex3h8 909	Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
u = (p⊥ ∩ q)    &   w = q⊥    ⇒   u ≤ w⊥
Theorem	gomaex3h9 910	Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
w = q⊥    &   x = q    ⇒   w ≤ x⊥
Theorem	gomaex3h10 911	Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥    &   x = q    &   y = (e ∪ f)⊥    ⇒   x ≤ y⊥
Theorem	gomaex3h11 912	Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
y = (e ∪ f)⊥    &   z = f    ⇒   y ≤ z⊥
Theorem	gomaex3h12 913	Hypothesis for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
f ≤ a⊥    &   g = a    &   z = f    ⇒   z ≤ g⊥
Theorem	gomaex3lem1 914	Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
c ≤ d⊥    ⇒   (c ∪ (c ∪ d)⊥ ) = d⊥
Theorem	gomaex3lem2 915	Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
e ≤ f⊥    ⇒   ((e ∪ f)⊥ ∪ f) = e⊥
Theorem	gomaex3lem3 916	Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
((p⊥ →1 q)⊥ ∪ (p⊥ ∩ q)) = p⊥
Theorem	gomaex3lem4 917	Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
p = ((a ∪ b) →1 (d ∪ e)⊥ )⊥    ⇒   ((a ∪ b) ∩ (d ∪ e)⊥ ) ≤ p⊥
Theorem	gomaex3lem5 918	Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
a ≤ b⊥    &   b ≤ c⊥    &   c ≤ d⊥    &   e ≤ f⊥    &   f ≤ a⊥    &   (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)    &   p = ((a ∪ b) →1 (d ∪ e)⊥ )⊥    &   q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥    &   r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))    &   g = a    &   h = b    &   i = c    &   j = (c ∪ d)⊥    &   k = r    &   m = (p⊥ →1 q)    &   n = (p⊥ →1 q)⊥    &   u = (p⊥ ∩ q)    &   w = q⊥    &   x = q    &   y = (e ∪ f)⊥    &   z = f    ⇒   (((g ∪ h) ∩ (i ∪ j)) ∩ (((k ∪ m) ∩ (n ∪ u)) ∩ ((w ∪ x) ∩ (y ∪ z)))) ≤ (h ∪ i)
Theorem	gomaex3lem6 919	Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
a ≤ b⊥    &   b ≤ c⊥    &   c ≤ d⊥    &   e ≤ f⊥    &   f ≤ a⊥    &   (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)    &   p = ((a ∪ b) →1 (d ∪ e)⊥ )⊥    &   q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥    &   r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))    &   g = a    &   h = b    &   i = c    &   j = (c ∪ d)⊥    &   k = r    &   m = (p⊥ →1 q)    &   n = (p⊥ →1 q)⊥    &   u = (p⊥ ∩ q)    &   w = q⊥    &   x = q    &   y = (e ∪ f)⊥    &   z = f    ⇒   (((a ∪ b) ∩ (c ∪ (c ∪ d)⊥ )) ∩ (((r ∪ (p⊥ →1 q)) ∩ ((p⊥ →1 q)⊥ ∪ (p⊥ ∩ q))) ∩ ((q⊥ ∪ q) ∩ ((e ∪ f)⊥ ∪ f)))) ≤ (b ∪ c)
Theorem	gomaex3lem7 920	Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
a ≤ b⊥    &   b ≤ c⊥    &   c ≤ d⊥    &   e ≤ f⊥    &   f ≤ a⊥    &   (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)    &   p = ((a ∪ b) →1 (d ∪ e)⊥ )⊥    &   q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥    &   r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))    &   g = a    &   h = b    &   i = c    &   j = (c ∪ d)⊥    &   k = r    &   m = (p⊥ →1 q)    &   n = (p⊥ →1 q)⊥    &   u = (p⊥ ∩ q)    &   w = q⊥    &   x = q    &   y = (e ∪ f)⊥    &   z = f    ⇒   (((a ∪ b) ∩ d⊥ ) ∩ (((r ∪ (p⊥ →1 q)) ∩ p⊥ ) ∩ e⊥ )) ≤ (b ∪ c)
Theorem	gomaex3lem8 921	Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
a ≤ b⊥    &   b ≤ c⊥    &   c ≤ d⊥    &   e ≤ f⊥    &   f ≤ a⊥    &   (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)    &   p = ((a ∪ b) →1 (d ∪ e)⊥ )⊥    &   q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥    &   r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))    &   g = a    &   h = b    &   i = c    &   j = (c ∪ d)⊥    &   k = r    &   m = (p⊥ →1 q)    &   n = (p⊥ →1 q)⊥    &   u = (p⊥ ∩ q)    &   w = q⊥    &   x = q    &   y = (e ∪ f)⊥    &   z = f    ⇒   (((a ∪ b) ∩ (d ∪ e)⊥ ) ∩ ((r ∪ (p⊥ →1 q)) ∩ p⊥ )) ≤ (b ∪ c)
Theorem	gomaex3lem9 922	Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
a ≤ b⊥    &   b ≤ c⊥    &   c ≤ d⊥    &   e ≤ f⊥    &   f ≤ a⊥    &   (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)    &   p = ((a ∪ b) →1 (d ∪ e)⊥ )⊥    &   q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥    &   r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))    &   g = a    &   h = b    &   i = c    &   j = (c ∪ d)⊥    &   k = r    &   m = (p⊥ →1 q)    &   n = (p⊥ →1 q)⊥    &   u = (p⊥ ∩ q)    &   w = q⊥    &   x = q    &   y = (e ∪ f)⊥    &   z = f    ⇒   (((a ∪ b) ∩ (d ∪ e)⊥ ) ∩ (r ∪ (p⊥ →1 q))) ≤ (b ∪ c)
Theorem	gomaex3lem10 923	Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)
a ≤ b⊥    &   b ≤ c⊥    &   c ≤ d⊥    &   e ≤ f⊥    &   f ≤ a⊥    &   (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)    &   p = ((a ∪ b) →1 (d ∪ e)⊥ )⊥    &   q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥    &   r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))    &   g = a    &   h = b    &   i = c    &   j = (c ∪ d)⊥    &   k = r    &   m = (p⊥ →1 q)    &   n = (p⊥ →1 q)⊥    &   u = (p⊥ ∩ q)    &   w = q⊥    &   x = q    &   y = (e ∪ f)⊥    &   z = f    ⇒   (((a ∪ b) ∩ (d ∪ e)⊥ ) ∩ (r ∪ (p⊥ →1 q))) ≤ ((b ∪ c) ∪ (e ∪ f)⊥ )
Theorem	gomaex3 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.)
a ≤ b⊥    &   b ≤ c⊥    &   c ≤ d⊥    &   e ≤ f⊥    &   f ≤ a⊥    &   (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)    &   p = ((a ∪ b) →1 (d ∪ e)⊥ )⊥    &   q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥    &   r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))    &   g = a    &   i = c    &   k = r    &   n = (p⊥ →1 q)⊥    &   w = q⊥    &   y = (e ∪ f)⊥    ⇒   (((a ∪ b) ∩ (d ∪ e)⊥ ) ∩ ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ →1 (c ∪ d))) ≤ ((b ∪ c) ∪ (e ∪ f)⊥ )
0.3.11  OML Lemmas for studying orthoarguesian laws
Theorem	oas 925	"Strengthening" lemma for studying the orthoarguesian law. (Contributed by NM, 25-Dec-1998.)
(a⊥ ∩ (a ∪ b)) ≤ c    ⇒   ((a →1 c) ∩ (a ∪ b)) ≤ c
Theorem	oasr 926	Reverse of oas 925 lemma for studying the orthoarguesian law. (Contributed by NM, 28-Dec-1998.)
((a →1 c) ∩ (a ∪ b)) ≤ c    ⇒   (a⊥ ∩ (a ∪ b)) ≤ c
Theorem	oat 927	Transformation lemma for studying the orthoarguesian law. (Contributed by NM, 26-Dec-1998.)
(a⊥ ∩ (a ∪ b)) ≤ c    ⇒   b ≤ (a⊥ →1 c)
Theorem	oatr 928	Reverse transformation lemma for studying the orthoarguesian law. (Contributed by NM, 26-Dec-1998.)
b ≤ (a⊥ →1 c)    ⇒   (a⊥ ∩ (a ∪ b)) ≤ c
Theorem	oau 929	Transformation lemma for studying the orthoarguesian law. (Contributed by NM, 28-Dec-1998.)
(a ∩ ((a →1 c) ∪ b)) ≤ c    ⇒   b ≤ (a →1 c)
Theorem	oaur 930	Transformation lemma for studying the orthoarguesian law. (Contributed by NM, 28-Dec-1998.)
b ≤ (a →1 c)    ⇒   (a ∩ ((a →1 c) ∪ b)) ≤ c
Theorem	oaidlem2 931	Lemma for identity-like OA law. (Contributed by NM, 22-Jan-1999.)
((d ∪ ((a →1 c) ∩ (b →1 c)))⊥ ∪ ((a →1 c) →1 (b →1 c))) = 1    ⇒   ((a →1 c) ∩ (d ∪ ((a →1 c) ∩ (b →1 c)))) ≤ (b →1 c)
Theorem	oaidlem2g 932	Lemma for identity-like OA law (generalized). (Contributed by NM, 18-Feb-2002.)
((c ∪ (a ∩ b))⊥ ∪ (a →1 b)) = 1    ⇒   (a ∩ (c ∪ (a ∩ b))) ≤ b
Theorem	oa6v4v 933	6-variable OA to 4-variable OA. (Contributed by NM, 29-Nov-1998.)
(((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) ≤ (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))))    &   e = 0    &   f = 1    ⇒   ((a ∪ b) ∩ (c ∪ d)) ≤ (b ∪ (a ∩ (c ∪ ((a ∪ c) ∩ (b ∪ d)))))
Theorem	oa4v3v 934	4-variable OA to 3-variable OA (Godowski/Greechie Eq. IV). (Contributed by NM, 28-Nov-1998.)
d ≤ b⊥    &   e ≤ c⊥    &   ((d ∪ b) ∩ (e ∪ c)) ≤ (b ∪ (d ∩ (e ∪ ((d ∪ e) ∩ (b ∪ c)))))    &   d = (a →2 b)⊥    &   e = (a →2 c)⊥    ⇒   (b⊥ ∩ ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))))) ≤ ((b⊥ ∩ (a →2 b)) ∪ (c⊥ ∩ (a →2 c)))
Theorem	oal42 935	Derivation of Godowski/Greechie Eq. II from Eq. IV. (Contributed by NM, 25-Nov-1998.)
(b⊥ ∩ ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))))) ≤ ((b⊥ ∩ (a →2 b)) ∪ (c⊥ ∩ (a →2 c)))    ⇒   (b⊥ ∩ ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))))) ≤ a⊥
Theorem	oa23 936	Derivation of OA from Godowski/Greechie Eq. II. (Contributed by NM, 25-Nov-1998.)
(c⊥ ∩ ((a →2 c) ∪ ((a →2 b) ∩ ((c ∪ b)⊥ ∪ ((a →2 c) ∩ (a →2 b)))))) ≤ a⊥    ⇒   ((a →2 b) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))) ≤ (a →2 c)
Theorem	oa4lem1 937	Lemma for 3-var to 4-var OA. (Contributed by NM, 27-Nov-1998.)
a ≤ b⊥    &   c ≤ d⊥    ⇒   (a ∪ b) ≤ ((a ∪ c)⊥ →2 b)
Theorem	oa4lem2 938	Lemma for 3-var to 4-var OA. (Contributed by NM, 27-Nov-1998.)
a ≤ b⊥    &   c ≤ d⊥    ⇒   (c ∪ d) ≤ ((a ∪ c)⊥ →2 d)
Theorem	oa4lem3 939	Lemma for 3-var to 4-var OA. (Contributed by NM, 27-Nov-1998.)
a ≤ b⊥    &   c ≤ d⊥    ⇒   ((a ∪ b) ∩ (c ∪ d)) ≤ ((b ∪ d)⊥ ∪ (((a ∪ c)⊥ →2 b) ∩ ((a ∪ c)⊥ →2 d)))
Theorem	distoah1 940	Satisfaction of distributive law hypothesis. (Contributed by NM, 29-Nov-1998.)
d = (a →2 b)    &   e = ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))    &   f = ((b ∪ c) →2 ((a →2 b) ∩ (a →2 c)))    ⇒   d ≤ (a →2 b)
Theorem	distoah2 941	Satisfaction of distributive law hypothesis. (Contributed by NM, 29-Nov-1998.)
d = (a →2 b)    &   e = ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))    &   f = ((b ∪ c) →2 ((a →2 b) ∩ (a →2 c)))    ⇒   e ≤ ((b ∪ c) →0 ((a →2 b) ∩ (a →2 c)))
Theorem	distoah3 942	Satisfaction of distributive law hypothesis. (Contributed by NM, 29-Nov-1998.)
d = (a →2 b)    &   e = ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))    &   f = ((b ∪ c) →2 ((a →2 b) ∩ (a →2 c)))    ⇒   f ≤ ((b ∪ c) →0 ((a →2 b) ∩ (a →2 c)))
Theorem	distoah4 943	Satisfaction of distributive law hypothesis. (Contributed by NM, 29-Nov-1998.)
d = (a →2 b)    &   e = ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))    &   f = ((b ∪ c) →2 ((a →2 b) ∩ (a →2 c)))    ⇒   (d ∩ (a →2 c)) ≤ f
Theorem	distoa 944	Derivation in OM of OA, assuming OA distributive law oadistd 1023. (Contributed by NM, 29-Nov-1998.)
d = (a →2 b)    &   e = ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))    &   f = ((b ∪ c) →2 ((a →2 b) ∩ (a →2 c)))    &   (d ∩ (e ∪ f)) = ((d ∩ e) ∪ (d ∩ f))    ⇒   ((a →2 b) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))) ≤ (a →2 c)
Theorem	oa3to4lem1 945	Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof). (Contributed by NM, 19-Dec-1998.)
a⊥ ≤ b    &   c⊥ ≤ d    &   g = ((a ∩ b) ∪ (c ∩ d))    ⇒   b ≤ (a →1 g)
Theorem	oa3to4lem2 946	Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof). (Contributed by NM, 19-Dec-1998.)
a⊥ ≤ b    &   c⊥ ≤ d    &   g = ((a ∩ b) ∪ (c ∩ d))    ⇒   d ≤ (c →1 g)
Theorem	oa3to4lem3 947	Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof). (Contributed by NM, 19-Dec-1998.)
a⊥ ≤ b    &   c⊥ ≤ d    &   g = ((a ∩ b) ∪ (c ∩ d))    ⇒   (a ∩ (b ∪ (d ∩ ((a ∩ c) ∪ (b ∩ d))))) ≤ (a ∩ ((a →1 g) ∪ ((c →1 g) ∩ ((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))))))
Theorem	oa3to4lem4 948	Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof). (Contributed by NM, 19-Dec-1998.)
a⊥ ≤ b    &   c⊥ ≤ d    &   g = ((a ∩ b) ∪ (c ∩ d))    &   (a ∩ ((a →1 g) ∪ ((c →1 g) ∩ ((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g)))))) ≤ ((a ∩ g) ∪ (c ∩ g))    ⇒   (a ∩ (b ∪ (d ∩ ((a ∩ c) ∪ (b ∩ d))))) ≤ g
Theorem	oa3to4lem5 949	Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof). (Contributed by NM, 19-Dec-1998.)
((a ∪ b) ∩ (c ∪ d)) ≤ (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))    ⇒   ((b ∪ a) ∩ (d ∪ c)) ≤ (a ∪ (b ∩ (d ∪ ((b ∪ d) ∩ (a ∪ c)))))
Theorem	oa3to4lem6 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.)
a ≤ b⊥    &   c ≤ d⊥    &   g = ((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ ))    &   e = a⊥    &   f = c⊥    &   (e ∩ ((e →1 g) ∪ ((f →1 g) ∩ ((e ∩ f) ∪ ((e →1 g) ∩ (f →1 g)))))) ≤ ((e ∩ g) ∪ (f ∩ g))    ⇒   ((a ∪ b) ∩ (c ∪ d)) ≤ (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))
Theorem	oa3to4 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.)
a ≤ b⊥    &   c ≤ d⊥    &   g = ((b⊥ ∩ a⊥ ) ∪ (d⊥ ∩ c⊥ ))    &   e = b⊥    &   f = d⊥    &   (e ∩ ((e →1 g) ∪ ((f →1 g) ∩ ((e ∩ f) ∪ ((e →1 g) ∩ (f →1 g)))))) ≤ ((e ∩ g) ∪ (f ∩ g))    ⇒   ((a ∪ b) ∩ (c ∪ d)) ≤ (b ∪ (a ∩ (c ∪ ((a ∪ c) ∩ (b ∪ d)))))
Theorem	oa6todual 952	Conventional to dual 6-variable OA law. (Contributed by NM, 22-Dec-1998.)
(((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ (e⊥ ∪ f⊥ )) ≤ (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ (((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∪ ((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )))))))    ⇒   (b ∩ (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))))) ≤ (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))
Theorem	oa6fromdual 953	Dual to conventional 6-variable OA law. (Contributed by NM, 22-Dec-1998.)
(b⊥ ∩ (a⊥ ∪ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))))))) ≤ (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))    ⇒   (((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) ≤ (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))))
Theorem	oa6fromdualn 954	Dual to conventional 6-variable OA law. (Contributed by NM, 24-Dec-1998.)
(b ∩ (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))))) ≤ (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))    ⇒   (((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ (e⊥ ∪ f⊥ )) ≤ (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ (((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∪ ((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )))))))
Theorem	oa6to4h1 955	Satisfaction of 6-variable OA law hypothesis. (Contributed by NM, 22-Dec-1998.)
b⊥ = (a →1 g)⊥    &   d⊥ = (c →1 g)⊥    &   f⊥ = (e →1 g)⊥    ⇒   a⊥ ≤ b⊥ ⊥
Theorem	oa6to4h2 956	Satisfaction of 6-variable OA law hypothesis. (Contributed by NM, 22-Dec-1998.)
b⊥ = (a →1 g)⊥    &   d⊥ = (c →1 g)⊥    &   f⊥ = (e →1 g)⊥    ⇒   c⊥ ≤ d⊥ ⊥
Theorem	oa6to4h3 957	Satisfaction of 6-variable OA law hypothesis. (Contributed by NM, 22-Dec-1998.)
b⊥ = (a →1 g)⊥    &   d⊥ = (c →1 g)⊥    &   f⊥ = (e →1 g)⊥    ⇒   e⊥ ≤ f⊥ ⊥
Theorem	oa6to4 958	Derivation of 4-variable proper OA law, assuming 6-variable OA law. (Contributed by NM, 22-Dec-1998.)
b⊥ = (a →1 g)⊥    &   d⊥ = (c →1 g)⊥    &   f⊥ = (e →1 g)⊥    &   (((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ (e⊥ ∪ f⊥ )) ≤ (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ (((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∪ ((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )))))))    ⇒   ((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ (((a ∩ g) ∪ (c ∩ g)) ∪ (e ∩ g))
Theorem	oa4b 959	Derivation of 4-OA law variant. (Contributed by NM, 22-Dec-1998.)
((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ (((a ∩ g) ∪ (c ∩ g)) ∪ (e ∩ g))    ⇒   ((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ g
Theorem	oa4to6lem1 960	Lemma for orthoarguesian law (4-variable to 6-variable proof). (Contributed by NM, 18-Dec-1998.)
a⊥ ≤ b    &   c⊥ ≤ d    &   e⊥ ≤ f    &   g = (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))    ⇒   b ≤ (a →1 g)
Theorem	oa4to6lem2 961	Lemma for orthoarguesian law (4-variable to 6-variable proof). (Contributed by NM, 18-Dec-1998.)
a⊥ ≤ b    &   c⊥ ≤ d    &   e⊥ ≤ f    &   g = (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))    ⇒   d ≤ (c →1 g)
Theorem	oa4to6lem3 962	Lemma for orthoarguesian law (4-variable to 6-variable proof). (Contributed by NM, 18-Dec-1998.)
a⊥ ≤ b    &   c⊥ ≤ d    &   e⊥ ≤ f    &   g = (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))    ⇒   f ≤ (e →1 g)
Theorem	oa4to6lem4 963	Lemma for orthoarguesian law (4-variable to 6-variable proof). (Contributed by NM, 18-Dec-1998.)
a⊥ ≤ b    &   c⊥ ≤ d    &   e⊥ ≤ f    &   g = (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))    ⇒   (b ∩ (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))))) ≤ ((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g))))))))
Theorem	oa4to6dual 964	Lemma for orthoarguesian law (4-variable to 6-variable proof). (Contributed by NM, 19-Dec-1998.)
a⊥ ≤ b    &   c⊥ ≤ d    &   e⊥ ≤ f    &   g = (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))    &   ((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ g    ⇒   (b ∩ (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))))) ≤ g
Theorem	oa4to6 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.)
a ≤ b⊥    &   c ≤ d⊥    &   e ≤ f⊥    &   g = (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))    &   h = a⊥    &   j = c⊥    &   k = e⊥    &   ((h →1 g) ∩ (h ∪ (j ∩ (((h ∩ j) ∪ ((h →1 g) ∩ (j →1 g))) ∪ (((h ∩ k) ∪ ((h →1 g) ∩ (k →1 g))) ∩ ((j ∩ k) ∪ ((j →1 g) ∩ (k →1 g)))))))) ≤ g    ⇒   (((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) ≤ (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))))
Theorem	oa4btoc 966	Derivation of 4-OA law variant. (Contributed by NM, 22-Dec-1998.)
((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ g    ⇒   (a⊥ ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ g
Theorem	oa4ctob 967	Derivation of 4-OA law variant. (Contributed by NM, 22-Dec-1998.)
(a⊥ ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ g    ⇒   ((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ g
Theorem	oa4ctod 968	Derivation of 4-OA law variant. (Contributed by NM, 24-Dec-1998.)
(a⊥ ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d)))))))) ≤ d    ⇒   (b ∩ (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d)))))) ≤ (a⊥ →1 d)
Theorem	oa4dtoc 969	Derivation of 4-OA law variant. (Contributed by NM, 24-Dec-1998.)
(b ∩ (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d)))))) ≤ (a⊥ →1 d)    ⇒   (a⊥ ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d)))))))) ≤ d
Theorem	oa4dcom 970	Lemma commuting terms. (Contributed by NM, 24-Dec-1998.)
(b ∩ (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d)))))) = (b ∩ (((b ∩ a) ∪ ((b →1 d) ∩ (a →1 d))) ∪ (((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d))) ∩ ((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))))))
0.3.12  5OA law
Theorem	oa8todual 971	Conventional to dual 8-variable OA law. (Contributed by NM, 8-May-2000.)
(((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ ((e⊥ ∪ f⊥ ) ∩ (g⊥ ∪ h⊥ ))) ≤ (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))))))    ⇒   (b ∩ (a ∪ (c ∩ ((((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((c ∩ g) ∪ (d ∩ h)))) ∪ ((((a ∩ e) ∪ (b ∩ f)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) ∩ (((c ∩ e) ∪ (d ∩ f)) ∪ (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h))))))))) ≤ (((a ∩ b) ∪ (c ∩ d)) ∪ ((e ∩ f) ∪ (g ∩ h)))
Theorem	oa8to5 972	Orthoarguesian law 5OA converted from 8 to 5 variables. (Contributed by NM, 8-May-2000.)
(((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ ((e⊥ ∪ f⊥ ) ∩ (g⊥ ∪ h⊥ ))) ≤ (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))))))    &   b⊥ = (a →1 j)⊥    &   d⊥ = (c →1 j)⊥    &   f⊥ = (e →1 j)⊥    &   h⊥ = (g →1 j)⊥    ⇒   ((a →1 j) ∩ (a ∪ (c ∩ ((((a ∩ c) ∪ ((a →1 j) ∩ (c →1 j))) ∪ (((a ∩ g) ∪ ((a →1 j) ∩ (g →1 j))) ∩ ((c ∩ g) ∪ ((c →1 j) ∩ (g →1 j))))) ∪ ((((a ∩ e) ∪ ((a →1 j) ∩ (e →1 j))) ∪ (((a ∩ g) ∪ ((a →1 j) ∩ (g →1 j))) ∩ ((e ∩ g) ∪ ((e →1 j) ∩ (g →1 j))))) ∩ (((c ∩ e) ∪ ((c →1 j) ∩ (e →1 j))) ∪ (((c ∩ g) ∪ ((c →1 j) ∩ (g →1 j))) ∩ ((e ∩ g) ∪ ((e →1 j) ∩ (g →1 j)))))))))) ≤ (((a ∩ j) ∪ (c ∩ j)) ∪ ((e ∩ j) ∪ (g ∩ j)))
0.3.13  "Godowski/Greechie" form of proper 4-OA
Theorem	oa4to4u 973	A "universal" 4-OA. The hypotheses are the standard proper 4-OA and substitutions into it. (Contributed by NM, 28-Dec-1998.)
((e →1 d) ∩ (e ∪ (f ∩ (((e ∩ f) ∪ ((e →1 d) ∩ (f →1 d))) ∪ (((e ∩ g) ∪ ((e →1 d) ∩ (g →1 d))) ∩ ((f ∩ g) ∪ ((f →1 d) ∩ (g →1 d)))))))) ≤ (((e ∩ d) ∪ (f ∩ d)) ∪ (g ∩ d))    &   e = (a⊥ →1 d)    &   f = (b⊥ →1 d)    &   g = (c⊥ →1 d)    ⇒   ((a →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))))))) ≤ ((((a →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (b⊥ →1 d))) ∪ ((c →1 d) ∩ (c⊥ →1 d)))
Theorem	oa4to4u2 974	A weaker-looking "universal" proper 4-OA. (Contributed by NM, 29-Dec-1998.)
((e →1 d) ∩ (e ∪ (f ∩ (((e ∩ f) ∪ ((e →1 d) ∩ (f →1 d))) ∪ (((e ∩ g) ∪ ((e →1 d) ∩ (g →1 d))) ∩ ((f ∩ g) ∪ ((f →1 d) ∩ (g →1 d)))))))) ≤ (((e ∩ d) ∪ (f ∩ d)) ∪ (g ∩ d))    &   e = (a⊥ →1 d)    &   f = (b⊥ →1 d)    &   g = (c⊥ →1 d)    ⇒   ((a →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))))))) ≤ d
Theorem	oa4uto4g 975	Derivation of "Godowski/Greechie" 4-variable proper OA law variant from "universal" variant oa4to4u2 974. (Contributed by NM, 28-Dec-1998.)
((b⊥ →1 d) ∩ ((b⊥ ⊥ →1 d) ∪ ((a⊥ ⊥ →1 d) ∩ ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (a⊥ ⊥ →1 d))) ∪ ((((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d))) ∩ (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d)))))))) ≤ d    &   h = (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d))))    ⇒   ((a →1 d) ∩ (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ h)) ≤ (b →1 d)
Theorem	oa4gto4u 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.)
((e →1 d) ∩ (((e ∩ f) ∪ ((e →1 d) ∩ (f →1 d))) ∪ (((e ∩ g) ∪ ((e →1 d) ∩ (g →1 d))) ∩ ((f ∩ g) ∪ ((f →1 d) ∩ (g →1 d)))))) ≤ (f →1 d)    &   f = (a →1 d)    &   e = (b →1 d)    &   g = (c →1 d)    ⇒   ((a →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))))))) ≤ d
Theorem	oa4uto4 977	Derivation of standard 4-variable proper OA law from "universal" variant oa4to4u2 974. (Contributed by NM, 30-Dec-1998.)
((a →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))))))) ≤ d    ⇒   ((a →1 d) ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d)))))))) ≤ d
0.3.14  Some 3-OA inferences (derived under OM)
Theorem	oa3-2lema 978	Lemma for 3-OA(2). Equivalence with substitution into 4-OA. (Contributed by NM, 24-Dec-1998.)
((a →1 c) ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c))) ∪ (((a ∩ 0) ∪ ((a →1 c) ∩ (0 →1 c))) ∩ ((b ∩ 0) ∪ ((b →1 c) ∩ (0 →1 c)))))))) = ((a →1 c) ∩ (a ∪ (b ∩ ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c))))))
Theorem	oa3-2lemb 979	Lemma for 3-OA(2). Equivalence with substitution into 4-OA. (Contributed by NM, 24-Dec-1998.)
((a →1 c) ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c))) ∪ (((a ∩ c) ∪ ((a →1 c) ∩ (c →1 c))) ∩ ((b ∩ c) ∪ ((b →1 c) ∩ (c →1 c)))))))) = ((a →1 c) ∩ (a ∪ (b ∩ ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c))))))
Theorem	oa3-6lem 980	Lemma for 3-OA(6). Equivalence with substitution into 4-OA. (Contributed by NM, 24-Dec-1998.)
((a →1 c) ∩ (a ∪ (b ∩ (((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c))) ∪ (((a ∩ 1) ∪ ((a →1 c) ∩ (1 →1 c))) ∩ ((b ∩ 1) ∪ ((b →1 c) ∩ (1 →1 c)))))))) = ((a →1 c) ∩ (a ∪ (b ∩ (((a⊥ →1 c) ∩ (b⊥ →1 c)) ∪ ((a →1 c) ∩ (b →1 c))))))
Theorem	oa3-3lem 981	Lemma for 3-OA(3). Equivalence with substitution into 6-OA dual. (Contributed by NM, 24-Dec-1998.)
(a⊥ ∩ (a ∪ (b ∩ (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (((a ∩ 1) ∪ (a⊥ ∩ c)) ∩ ((b ∩ 1) ∪ (b⊥ ∩ c))))))) = (a⊥ ∩ (a ∪ (b ∩ ((a ≡ b) ∪ ((a⊥ →1 c) ∩ (b⊥ →1 c))))))
Theorem	oa3-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 ∩ (a →1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b →1 c))) ∩ ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c)))))))) = (a ∩ ((a →1 c) ∪ ((b →1 c) ∩ ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c))))))
Theorem	oa3-4lem 983	Lemma for 3-OA(4). Equivalence with substitution into 6-OA dual. (Contributed by NM, 25-Dec-1998.)
(a⊥ ∩ (a ∪ (b ∩ (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (((a ∩ c) ∪ (a⊥ ∩ 1)) ∩ ((b ∩ c) ∪ (b⊥ ∩ 1))))))) = (a⊥ ∩ (a ∪ (b ∩ ((a ≡ b) ∪ ((a →1 c) ∩ (b →1 c))))))
Theorem	oa3-5lem 984	Lemma for 3-OA(5). Equivalence with substitution into 6-OA dual. (Contributed by NM, 25-Dec-1998.)
((a →1 c) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 c) ∩ 1)) ∪ (((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c))) ∩ ((c ∩ b) ∪ (1 ∩ (b →1 c)))))))) = ((a →1 c) ∩ (a ∪ (c ∩ ((a →1 c) ∪ ((b →1 c) ∩ ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c))))))))
Theorem	oa3-u1lem 985	Lemma for a "universal" 3-OA. Equivalence with substitution into 6-OA dual. (Contributed by NM, 26-Dec-1998.)
(1 ∩ (c ∪ ((a⊥ →1 c) ∩ (((c ∩ (a⊥ →1 c)) ∪ (1 ∩ (a →1 c))) ∪ (((c ∩ (b⊥ →1 c)) ∪ (1 ∩ (b →1 c))) ∩ (((a⊥ →1 c) ∩ (b⊥ →1 c)) ∪ ((a →1 c) ∩ (b →1 c)))))))) = (c ∪ ((a⊥ →1 c) ∩ ((a →1 c) ∪ ((b →1 c) ∩ (((a →1 c) ∩ (b →1 c)) ∪ ((a⊥ →1 c) ∩ (b⊥ →1 c)))))))
Theorem	oa3-u2lem 986	Lemma for a "universal" 3-OA. Equivalence with substitution into 6-OA dual. (Contributed by NM, 27-Dec-1998.)
((a →1 c) ∩ ((a⊥ →1 c) ∪ (c ∩ ((((a⊥ →1 c) ∩ c) ∪ ((a →1 c) ∩ 1)) ∪ ((((a⊥ →1 c) ∩ (b⊥ →1 c)) ∪ ((a →1 c) ∩ (b →1 c))) ∩ ((c ∩ (b⊥ →1 c)) ∪ (1 ∩ (b →1 c)))))))) = ((a →1 c) ∩ ((a⊥ →1 c) ∪ (c ∩ ((a →1 c) ∪ ((b →1 c) ∩ (((a →1 c) ∩ (b →1 c)) ∪ ((a⊥ →1 c) ∩ (b⊥ →1 c))))))))
Theorem	oa3-6to3 987	Derivation of 3-OA variant (3) from (6). (Contributed by NM, 24-Dec-1998.)
((a →1 c) ∩ (a ∪ (b ∩ (((a⊥ →1 c) ∩ (b⊥ →1 c)) ∪ ((a →1 c) ∩ (b →1 c)))))) ≤ c    ⇒   (a⊥ ∩ (a ∪ (b ∩ ((a ≡ b) ∪ ((a⊥ →1 c) ∩ (b⊥ →1 c)))))) ≤ c
Theorem	oa3-2to4 988	Derivation of 3-OA variant (4) from (2). (Contributed by NM, 24-Dec-1998.)
((a →1 c) ∩ (a ∪ (b ∩ ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c)))))) ≤ c    ⇒   (a⊥ ∩ (a ∪ (b ∩ ((a ≡ b) ∪ ((a →1 c) ∩ (b →1 c)))))) ≤ c
Theorem	oa3-2wto2 989	Derivation of 3-OA variant from weaker version. (Contributed by NM, 25-Dec-1998.)
(a⊥ ∩ (a ∪ (b ∩ ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c)))))) ≤ c    ⇒   ((a →1 c) ∩ (a ∪ (b ∩ ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c)))))) ≤ c
Theorem	oa3-2to2s 990	Derivation of 3-OA variant from weaker version. (Contributed by NM, 25-Dec-1998.)
((a →1 d) ∩ (a ∪ (b ∩ ((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d)))))) ≤ d    &   d = ((a ∩ c) ∪ (b ∩ c))    ⇒   ((a →1 c) ∩ (a ∪ (b ∩ ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c)))))) ≤ ((a ∩ c) ∪ (b ∩ c))
Theorem	oa3-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.)
((c →1 c) ∩ (c ∪ ((a⊥ →1 c) ∩ (((c ∩ (a⊥ →1 c)) ∪ ((c →1 c) ∩ ((a⊥ →1 c) →1 c))) ∪ (((c ∩ (b⊥ →1 c)) ∪ ((c →1 c) ∩ ((b⊥ →1 c) →1 c))) ∩ (((a⊥ →1 c) ∩ (b⊥ →1 c)) ∪ (((a⊥ →1 c) →1 c) ∩ ((b⊥ →1 c) →1 c)))))))) ≤ c    ⇒   (c ∪ ((a⊥ →1 c) ∩ ((a →1 c) ∪ ((b →1 c) ∩ (((a →1 c) ∩ (b →1 c)) ∪ ((a⊥ →1 c) ∩ (b⊥ →1 c))))))) ≤ c
Theorem	oa3-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.)
(((a⊥ →1 c) →1 c) ∩ ((a⊥ →1 c) ∪ (c ∩ ((((a⊥ →1 c) ∩ c) ∪ (((a⊥ →1 c) →1 c) ∩ (c →1 c))) ∪ ((((a⊥ →1 c) ∩ (b⊥ →1 c)) ∪ (((a⊥ →1 c) →1 c) ∩ ((b⊥ →1 c) →1 c))) ∩ ((c ∩ (b⊥ →1 c)) ∪ ((c →1 c) ∩ ((b⊥ →1 c) →1 c)))))))) ≤ c    ⇒   ((a →1 c) ∩ ((a⊥ →1 c) ∪ (c ∩ ((a →1 c) ∪ ((b →1 c) ∩ (((a →1 c) ∩ (b →1 c)) ∪ ((a⊥ →1 c) ∩ (b⊥ →1 c)))))))) ≤ c
Theorem	oa3-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.)
((a →1 c) ∩ ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c)))) ≤ (b →1 c)    ⇒   (c ∩ ((b →1 c) ∪ ((a →1 c) ∩ ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c)))))) ≤ (b⊥ →1 c)
0.4  Derivation of 4-variable proper OA from OA distributive law
Axiom	ax-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 = (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d))))    &   f = (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ e)    &   h ≤ (a →1 d)    &   j ≤ f    &   k ≤ f    &   (h ∩ (b →1 d)) ≤ k    ⇒   (h ∩ (j ∪ k)) = ((h ∩ j) ∪ (h ∩ k))
Theorem	d3oa 995	Derivation of 3-OA from OA distributive law. (Contributed by NM, 30-Dec-1998.)
f = ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c)))    ⇒   ((a →1 c) ∩ f) ≤ (b →1 c)
Theorem	d4oa 996	Variant of proper 4-OA proved from OA distributive law. (Contributed by NM, 30-Dec-1998.)
e = ((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d)))    &   f = (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d))))    ⇒   ((a →1 d) ∩ (e ∪ f)) ≤ (b →1 d)
Theorem	d6oa 997	Derivation of 6-variable orthoarguesian law from OA distributive law. (Contributed by NM, 30-Dec-1998.)
a ≤ b⊥    &   c ≤ d⊥    &   e ≤ f⊥    ⇒   (((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) ≤ (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))))
0.5  Orthoarguesian laws
0.5.1  3-variable orthoarguesian law
Axiom	ax-3oa 998	3-variable consequence of the orthoarguesion law. (Contributed by NM, 20-Jul-1999.)
((a →1 c) ∩ ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c)))) ≤ (b →1 c)
Theorem	oal2 999	Orthoarguesian law - →2 version. (Contributed by NM, 20-Jul-1999.)
((a →2 b) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))) ≤ (a →2 c)
Theorem	oal1 1000	Orthoarguesian law - →1 version derived from →1 version. (Contributed by NM, 25-Nov-1998.)
((a →1 c) ∩ ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c)))) ≤ (b →1 c)