Theorem hlatcon3

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

	Ref	Expression
Hypotheses	3noncol.l	|- .<_ = ( le ` K )
	3noncol.j	|- .\/ = ( join ` K )
	3noncol.a	|- A = ( Atoms ` K )
Assertion	hlatcon3	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> -. P .<_ ( Q .\/ R ) )

Proof

Step	Hyp	Ref	Expression
1		3noncol.l	|- .<_ = ( le ` K )
2		3noncol.j	|- .\/ = ( join ` K )
3		3noncol.a	|- A = ( Atoms ` K )
4	1 2 3	3noncolr2	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( Q =/= R /\ -. P .<_ ( Q .\/ R ) ) )
5	4	simprd	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> -. P .<_ ( Q .\/ R ) )