Metamath Proof Explorer


Theorem atleneN

Description: Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 atlene.l ˙ = K
2 atlene.j ˙ = join K
3 atlene.a A = Atoms K
4 eqid K = K
5 1 2 4 3 atcvrj1 K HL P A Q A R A P R P ˙ Q ˙ R P K Q ˙ R
6 2 4 3 atcvrneN K HL P A Q A R A P K Q ˙ R Q R
7 5 6 syld3an3 K HL P A Q A R A P R P ˙ Q ˙ R Q R