hlatcon3

Description: Atom exchange combined with contraposition. (Contributed by NM, 13-Jun-2012)

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

Step	Hyp	Ref	Expression
1		3noncol.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		3noncol.j	$⊢ \underset{˙}{\lor} = join (K)$
3		3noncol.a	$⊢ A = Atoms (K)$
4	1 2 3	3noncolr2	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (Q \neq R \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
5	4	simprd	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$

Metamath Proof Explorer