Metamath Proof Explorer


Theorem cmcm3ii

Description: Commutation with orthocomplement. Remark in Kalmbach p. 23. (Contributed by NM, 7-Aug-2004) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1 AC
pjoml2.2 BC
cmcmi.1 A𝐶B
Assertion cmcm3ii A𝐶B

Proof

Step Hyp Ref Expression
1 pjoml2.1 AC
2 pjoml2.2 BC
3 cmcmi.1 A𝐶B
4 1 2 cmcm3i A𝐶BA𝐶B
5 3 4 mpbi A𝐶B