Metamath Proof Explorer


Theorem 4atlem0be

Description: Lemma for 4at . (Contributed by NM, 10-Jul-2012)

Ref Expression
Hypotheses 4at.l ˙=K
4at.j ˙=joinK
4at.a A=AtomsK
Assertion 4atlem0be KHLPAQARA¬R˙P˙QPR

Proof

Step Hyp Ref Expression
1 4at.l ˙=K
2 4at.j ˙=joinK
3 4at.a A=AtomsK
4 simp1 KHLPAQARA¬R˙P˙QKHL
5 simp23 KHLPAQARA¬R˙P˙QRA
6 simp21 KHLPAQARA¬R˙P˙QPA
7 simp22 KHLPAQARA¬R˙P˙QQA
8 simp3 KHLPAQARA¬R˙P˙Q¬R˙P˙Q
9 1 2 3 atnlej1 KHLRAPAQA¬R˙P˙QRP
10 9 necomd KHLRAPAQA¬R˙P˙QPR
11 4 5 6 7 8 10 syl131anc KHLPAQARA¬R˙P˙QPR