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

Metamath Proof Explorer

Theorem cmcm2

Description: Commutation with orthocomplement. Theorem 2.3(i) of Beran p. 39. (Contributed by NM, 14-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion cmcm2 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝐶 ℋ B ↔ A 𝐶 ℋ ⊥ ⁡ B

Proof

Step Hyp Ref Expression
1 cmcm3 ⊢ B ∈ C ℋ ∧ A ∈ C ℋ → B 𝐶 ℋ A ↔ ⊥ ⁡ B 𝐶 ℋ A
2 1 ancoms ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → B 𝐶 ℋ A ↔ ⊥ ⁡ B 𝐶 ℋ A
3 cmcm ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝐶 ℋ B ↔ B 𝐶 ℋ A
4 choccl ⊢ B ∈ C ℋ → ⊥ ⁡ B ∈ C ℋ
5 cmcm ⊢ A ∈ C ℋ ∧ ⊥ ⁡ B ∈ C ℋ → A 𝐶 ℋ ⊥ ⁡ B ↔ ⊥ ⁡ B 𝐶 ℋ A
6 4 5 sylan2 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝐶 ℋ ⊥ ⁡ B ↔ ⊥ ⁡ B 𝐶 ℋ A
7 2 3 6 3bitr4d ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝐶 ℋ B ↔ A 𝐶 ℋ ⊥ ⁡ B