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	⊢ 𝐴 ∈ Cℋ
	fh1.2	⊢ 𝐵 ∈ Cℋ
	fh1.3	⊢ 𝐶 ∈ Cℋ
	fh1.4	⊢ 𝐴 𝐶ℋ 𝐵
	fh1.5	⊢ 𝐴 𝐶ℋ 𝐶
Assertion	cm2ji	⊢ 𝐴 𝐶ℋ ( 𝐵 ∨ℋ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fh1.1	⊢ 𝐴 ∈ Cℋ
2		fh1.2	⊢ 𝐵 ∈ Cℋ
3		fh1.3	⊢ 𝐶 ∈ Cℋ
4		fh1.4	⊢ 𝐴 𝐶ℋ 𝐵
5		fh1.5	⊢ 𝐴 𝐶ℋ 𝐶
6	1 2 3	3pm3.2i	⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ )
7	4 5	pm3.2i	⊢ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 )
8		cm2j	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → 𝐴 𝐶ℋ ( 𝐵 ∨ℋ 𝐶 ) )
9	6 7 8	mp2an	⊢ 𝐴 𝐶ℋ ( 𝐵 ∨ℋ 𝐶 )