Theorem lem3.3.7i0e2 1057

Description: Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 0, and this is the second part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Assertion

Ref	Expression
lem3.3.7i0e2	(a ≡0 (a ∩ b)) = ((a ∩ b) ≡0 a)

Proof of Theorem lem3.3.7i0e2

Step	Hyp	Ref	Expression
1		ancom 74	. 2 ((a⊥ ∪ (a ∩ b)) ∩ ((a ∩ b)⊥ ∪ a)) = (((a ∩ b)⊥ ∪ a) ∩ (a⊥ ∪ (a ∩ b)))
2		df-id0 49	. 2 (a ≡0 (a ∩ b)) = ((a⊥ ∪ (a ∩ b)) ∩ ((a ∩ b)⊥ ∪ a))
3		df-id0 49	. 2 ((a ∩ b) ≡0 a) = (((a ∩ b)⊥ ∪ a) ∩ (a⊥ ∪ (a ∩ b)))
4	1, 2, 3	3tr1 63	1 (a ≡0 (a ∩ b)) = ((a ∩ b) ≡0 a)

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7   ≡₀ wid0 17

This theorem was proved from axioms:  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37

This theorem depends on definitions:  df-a 40  df-id0 49

Copyright terms: Public domain