This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmdi2

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

Ref Expression
Assertion dmdi2 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ ∧ A 𝑀 ℋ * B ∧ B ⊆ C → C ∩ A ∨ ℋ B ⊆ C ∩ A ∨ ℋ B

Proof

Step Hyp Ref Expression
1 dmdi ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ ∧ A 𝑀 ℋ * B ∧ B ⊆ C → C ∩ A ∨ ℋ B = C ∩ A ∨ ℋ B
2 eqimss2 ⊢ C ∩ A ∨ ℋ B = C ∩ A ∨ ℋ B → C ∩ A ∨ ℋ B ⊆ C ∩ A ∨ ℋ B
3 1 2 syl ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ ∧ A 𝑀 ℋ * B ∧ B ⊆ C → C ∩ A ∨ ℋ B ⊆ C ∩ A ∨ ℋ B