Metamath Proof Explorer


Theorem hlatcon3

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

Ref Expression
Hypotheses 3noncol.l ˙ = K
3noncol.j ˙ = join K
3noncol.a A = Atoms K
Assertion hlatcon3 K HL P A Q A R A P Q ¬ R ˙ P ˙ Q ¬ P ˙ Q ˙ R

Proof

Step Hyp Ref Expression
1 3noncol.l ˙ = K
2 3noncol.j ˙ = join K
3 3noncol.a A = Atoms K
4 1 2 3 3noncolr2 K HL P A Q A R A P Q ¬ R ˙ P ˙ Q Q R ¬ P ˙ Q ˙ R
5 4 simprd K HL P A Q A R A P Q ¬ R ˙ P ˙ Q ¬ P ˙ Q ˙ R