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

Metamath Proof Explorer

Theorem cmcmii

Description: Commutation is symmetric. Theorem 2(v) of Kalmbach p. 22. (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 cmcmii ⊢ B 𝐶 ℋ A

Proof

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