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

Metamath Proof Explorer

Theorem cmcm2ii

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

Ref Expression
Hypotheses pjoml2.1 ⊢ A ∈ C ℋ
pjoml2.2 ⊢ B ∈ C ℋ
cmcmi.1 ⊢ A 𝐶 ℋ B
Assertion cmcm2ii ⊢ A 𝐶 ℋ ⊥ ⁡ B

Proof

Step Hyp Ref Expression
1 pjoml2.1 ⊢ A ∈ C ℋ
2 pjoml2.2 ⊢ B ∈ C ℋ
3 cmcmi.1 ⊢ A 𝐶 ℋ B
4 1 2 cmcm2i ⊢ A 𝐶 ℋ B ↔ A 𝐶 ℋ ⊥ ⁡ B
5 3 4 mpbi ⊢ A 𝐶 ℋ ⊥ ⁡ B