axoa4d - Quantum Logic Explorer

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

Theorem axoa4d 1038

Description: Proper 4-variable OA law variant. (Contributed by NM, 24-Dec-1998.)

**Assertion**
Ref	Expression
axoa4d	(a ∩ (((a ∩ b) ∪ ((a →₁d) ∩ (b →₁d))) ∪ (((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d))) ∩ ((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d)))))) ≤ (b^⊥ →₁d)

**Proof of Theorem axoa4d**
Step	Hyp	Ref	Expression
1		oa4dcom 970	. . 3 (a ∩ (((b ∩ a) ∪ ((b →₁d) ∩ (a →₁d))) ∪ (((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d))) ∩ ((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d)))))) = (a ∩ (((a ∩ b) ∪ ((a →₁d) ∩ (b →₁d))) ∪ (((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d))) ∩ ((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d))))))
2	1	ax-r1 35	. 2 (a ∩ (((a ∩ b) ∪ ((a →₁d) ∩ (b →₁d))) ∪ (((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d))) ∩ ((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d)))))) = (a ∩ (((b ∩ a) ∪ ((b →₁d) ∩ (a →₁d))) ∪ (((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d))) ∩ ((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d))))))
3		axoa4 1034	. . 3 (b^⊥ ∩ (b ∪ (a ∩ (((b ∩ a) ∪ ((b →₁d) ∩ (a →₁d))) ∪ (((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d))) ∩ ((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d)))))))) ≤ d
4	3	oa4ctod 968	. 2 (a ∩ (((b ∩ a) ∪ ((b →₁d) ∩ (a →₁d))) ∪ (((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d))) ∩ ((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d)))))) ≤ (b^⊥ →₁d)
5	2, 4	bltr 138	1 (a ∩ (((a ∩ b) ∪ ((a →₁d) ∩ (b →₁d))) ∪ (((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d))) ∩ ((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d)))))) ≤ (b^⊥ →₁d)

Colors of variables: term

Syntax hints: ≤ wle 2 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 →₁wi1 12

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 ax-4oa 1033

This theorem depends on definitions: df-b 39 df-a 40 df-t 41 df-f 42 df-i1 44 df-le1 130 df-le2 131 df-c1 132 df-c2 133

This theorem is referenced by: (None)