Metamath Proof Explorer


Theorem cm2ji

Description: A lattice element that commutes with two others also commutes with their join. Theorem 4.2 of Beran p. 49. (Contributed by NM, 11-May-2009) (New usage is discouraged.)

Ref Expression
Hypotheses fh1.1 AC
fh1.2 BC
fh1.3 CC
fh1.4 A𝐶B
fh1.5 A𝐶C
Assertion cm2ji A𝐶BC

Proof

Step Hyp Ref Expression
1 fh1.1 AC
2 fh1.2 BC
3 fh1.3 CC
4 fh1.4 A𝐶B
5 fh1.5 A𝐶C
6 1 2 3 3pm3.2i ACBCCC
7 4 5 pm3.2i A𝐶BA𝐶C
8 cm2j ACBCCCA𝐶BA𝐶CA𝐶BC
9 6 7 8 mp2an A𝐶BC