Metamath Proof Explorer


Theorem hlatcon2

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 hlatcon2 K HL P A Q A R A P Q ¬ R ˙ P ˙ Q ¬ P ˙ R ˙ Q

Proof

Step Hyp Ref Expression
1 3noncol.l ˙ = K
2 3noncol.j ˙ = join K
3 3noncol.a A = Atoms K
4 1 2 3 hlatcon3 K HL P A Q A R A P Q ¬ R ˙ P ˙ Q ¬ P ˙ Q ˙ R
5 simp1 K HL P A Q A R A P Q ¬ R ˙ P ˙ Q K HL
6 simp22 K HL P A Q A R A P Q ¬ R ˙ P ˙ Q Q A
7 simp23 K HL P A Q A R A P Q ¬ R ˙ P ˙ Q R A
8 2 3 hlatjcom K HL Q A R A Q ˙ R = R ˙ Q
9 5 6 7 8 syl3anc K HL P A Q A R A P Q ¬ R ˙ P ˙ Q Q ˙ R = R ˙ Q
10 9 breq2d K HL P A Q A R A P Q ¬ R ˙ P ˙ Q P ˙ Q ˙ R P ˙ R ˙ Q
11 4 10 mtbid K HL P A Q A R A P Q ¬ R ˙ P ˙ Q ¬ P ˙ R ˙ Q