Metamath Proof Explorer


Theorem cdleme0dN

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 13-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cdleme0.l ˙ = K
cdleme0.j ˙ = join K
cdleme0.m ˙ = meet K
cdleme0.a A = Atoms K
cdleme0.h H = LHyp K
cdleme0.u U = P ˙ Q ˙ W
cdleme0c.3 V = P ˙ R ˙ W
Assertion cdleme0dN K HL W H P A ¬ P ˙ W R A P R V A

Proof

Step Hyp Ref Expression
1 cdleme0.l ˙ = K
2 cdleme0.j ˙ = join K
3 cdleme0.m ˙ = meet K
4 cdleme0.a A = Atoms K
5 cdleme0.h H = LHyp K
6 cdleme0.u U = P ˙ Q ˙ W
7 cdleme0c.3 V = P ˙ R ˙ W
8 1 2 3 4 5 7 lhpat2 K HL W H P A ¬ P ˙ W R A P R V A