Metamath Proof Explorer


Theorem 3noncolr1N

Description: Two ways to express 3 non-colinear atoms (rotated right 1 place). (Contributed by NM, 12-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 3noncol.l ˙=K
3noncol.j ˙=joinK
3noncol.a A=AtomsK
Assertion 3noncolr1N KHLPAQARAPQ¬R˙P˙QRP¬Q˙R˙P

Proof

Step Hyp Ref Expression
1 3noncol.l ˙=K
2 3noncol.j ˙=joinK
3 3noncol.a A=AtomsK
4 simp1 KHLPAQARAPQ¬R˙P˙QKHL
5 simp22 KHLPAQARAPQ¬R˙P˙QQA
6 simp23 KHLPAQARAPQ¬R˙P˙QRA
7 simp21 KHLPAQARAPQ¬R˙P˙QPA
8 1 2 3 3noncolr2 KHLPAQARAPQ¬R˙P˙QQR¬P˙Q˙R
9 1 2 3 3noncolr2 KHLQARAPAQR¬P˙Q˙RRP¬Q˙R˙P
10 4 5 6 7 8 9 syl131anc KHLPAQARAPQ¬R˙P˙QRP¬Q˙R˙P