Metamath Proof Explorer


Theorem cmcm2

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

Ref Expression
Assertion cmcm2 A C B C A 𝐶 B A 𝐶 B

Proof

Step Hyp Ref Expression
1 cmcm3 B C A C B 𝐶 A B 𝐶 A
2 1 ancoms A C B C B 𝐶 A B 𝐶 A
3 cmcm A C B C A 𝐶 B B 𝐶 A
4 choccl B C B C
5 cmcm A C B C A 𝐶 B B 𝐶 A
6 4 5 sylan2 A C B C A 𝐶 B B 𝐶 A
7 2 3 6 3bitr4d A C B C A 𝐶 B A 𝐶 B