Metamath Proof Explorer


Theorem hlatexchb2

Description: A version of hlexchb2 for atoms. (Contributed by NM, 7-Feb-2012)

Ref Expression
Hypotheses hlatexchb.l ˙ = K
hlatexchb.j ˙ = join K
hlatexchb.a A = Atoms K
Assertion hlatexchb2 K HL P A Q A R A P R P ˙ Q ˙ R P ˙ R = Q ˙ R

Proof

Step Hyp Ref Expression
1 hlatexchb.l ˙ = K
2 hlatexchb.j ˙ = join K
3 hlatexchb.a A = Atoms K
4 hlcvl K HL K CvLat
5 1 2 3 cvlatexchb2 K CvLat P A Q A R A P R P ˙ Q ˙ R P ˙ R = Q ˙ R
6 4 5 syl3an1 K HL P A Q A R A P R P ˙ Q ˙ R P ˙ R = Q ˙ R