atleneN

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

	Ref	Expression
Hypotheses	atlene.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	atlene.j	$⊢ \underset{˙}{\lor} = join (K)$
	atlene.a	$⊢ A = Atoms (K)$
Assertion	atleneN	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to Q \neq R$

Step	Hyp	Ref	Expression
1		atlene.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		atlene.j	$⊢ \underset{˙}{\lor} = join (K)$
3		atlene.a	$⊢ A = Atoms (K)$
4		eqid	$⊢ ⋖_{K} = ⋖_{K}$
5	1 2 4 3	atcvrj1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to P ⋖_{K} (Q \underset{˙}{\lor} R)$
6	2 4 3	atcvrneN	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P ⋖_{K} (Q \underset{˙}{\lor} R)) \to Q \neq R$
7	5 6	syld3an3	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to Q \neq R$

Metamath Proof Explorer