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	|- A e. CH
	fh1.2	|- B e. CH
	fh1.3	|- C e. CH
	fh1.4	|- A C_H B
	fh1.5	|- A C_H C
Assertion	cm2ji	|- A C_H ( B vH C )

Proof

Step	Hyp	Ref	Expression
1		fh1.1	|- A e. CH
2		fh1.2	|- B e. CH
3		fh1.3	|- C e. CH
4		fh1.4	|- A C_H B
5		fh1.5	|- A C_H C
6	1 2 3	3pm3.2i	|- ( A e. CH /\ B e. CH /\ C e. CH )
7	4 5	pm3.2i	|- ( A C_H B /\ A C_H C )
8		cm2j	|- ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> A C_H ( B vH C ) )
9	6 7 8	mp2an	|- A C_H ( B vH C )