Theorem dmdi2

Description: Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005) (New usage is discouraged.)

	Ref	Expression
Assertion	dmdi2	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ* 𝐵 ∧ 𝐵 ⊆ 𝐶 ) ) → ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( 𝐶 ∩ 𝐴 ) ∨ℋ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dmdi	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ* 𝐵 ∧ 𝐵 ⊆ 𝐶 ) ) → ( ( 𝐶 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
2		eqimss2	⊢ ( ( ( 𝐶 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( 𝐶 ∩ 𝐴 ) ∨ℋ 𝐵 ) )
3	1 2	syl	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ* 𝐵 ∧ 𝐵 ⊆ 𝐶 ) ) → ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( 𝐶 ∩ 𝐴 ) ∨ℋ 𝐵 ) )