oa4dcom - Quantum Logic Explorer

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

Theorem oa4dcom 970

Description: Lemma commuting terms. (Contributed by NM, 24-Dec-1998.)

**Assertion**
Ref	Expression
oa4dcom	(b ∩ (((a ∩ b) ∪ ((a →₁d) ∩ (b →₁d))) ∪ (((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d))) ∩ ((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d)))))) = (b ∩ (((b ∩ a) ∪ ((b →₁d) ∩ (a →₁d))) ∪ (((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d))) ∩ ((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d))))))

**Proof of Theorem oa4dcom**
Step	Hyp	Ref	Expression
1		ancom 74	. . . 4 (a ∩ b) = (b ∩ a)
2		ancom 74	. . . 4 ((a →₁d) ∩ (b →₁d)) = ((b →₁d) ∩ (a →₁d))
3	1, 2	2or 72	. . 3 ((a ∩ b) ∪ ((a →₁d) ∩ (b →₁d))) = ((b ∩ a) ∪ ((b →₁d) ∩ (a →₁d)))
4		ancom 74	. . 3 (((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d))) ∩ ((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d)))) = (((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d))) ∩ ((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d))))
5	3, 4	2or 72	. 2 (((a ∩ b) ∪ ((a →₁d) ∩ (b →₁d))) ∪ (((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d))) ∩ ((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d))))) = (((b ∩ a) ∪ ((b →₁d) ∩ (a →₁d))) ∪ (((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d))) ∩ ((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d)))))
6	5	lan 77	1 (b ∩ (((a ∩ b) ∪ ((a →₁d) ∩ (b →₁d))) ∪ (((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d))) ∩ ((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d)))))) = (b ∩ (((b ∩ a) ∪ ((b →₁d) ∩ (a →₁d))) ∪ (((b ∩ c) ∪ ((b →₁d) ∩ (c →₁d))) ∩ ((a ∩ c) ∪ ((a →₁d) ∩ (c →₁d))))))

Colors of variables: term

This proof depends on syntax axioms: = wb 1 ∪ wo 6 ∩ wa 7 →₁wi1 12

This proof depends on axioms: ax-a2 31 ax-r1 35 ax-r2 36 ax-r4 37 ax-r5 38

This proof depends on definitions: df-a 40

This theorem is used by: axoa4d 1038