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

Metamath Proof Explorer

Theorem cmcmi

Description: Commutation is symmetric. Theorem 2(v) of Kalmbach p. 22. (Contributed by NM, 4-Nov-2000) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 pjoml2.1 ⊢ A ∈ C ℋ
2 pjoml2.2 ⊢ B ∈ C ℋ
3 1 2 cmcmlem ⊢ A 𝐶 ℋ B → B 𝐶 ℋ A
4 2 1 cmcmlem ⊢ B 𝐶 ℋ A → A 𝐶 ℋ B
5 3 4 impbii ⊢ A 𝐶 ℋ B ↔ B 𝐶 ℋ A