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


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