Metamath Proof Explorer


Theorem paddasslem1

Description: Lemma for paddass . (Contributed by NM, 8-Jan-2012)

Ref Expression
Hypotheses paddasslem.l ˙=K
paddasslem.j ˙=joinK
paddasslem.a A=AtomsK
Assertion paddasslem1 KHLxArAyAxy¬r˙x˙y¬x˙r˙y

Proof

Step Hyp Ref Expression
1 paddasslem.l ˙=K
2 paddasslem.j ˙=joinK
3 paddasslem.a A=AtomsK
4 1 2 3 hlatexch2 KHLxArAyAxyx˙r˙yr˙x˙y
5 4 con3dimp KHLxArAyAxy¬r˙x˙y¬x˙r˙y