Metamath Proof Explorer


Theorem cdleme46f2g2

Description: Conversion for G to reuse F theorems. TODO FIX COMMENT. TODO What other conversion theorems would be reused? e.g. cdlemeg46nlpq ? Find other hlatjcom uses giving Q .\/ P . (Contributed by NM, 1-Apr-2013)

Ref Expression
Hypotheses cdleme46fg.j ˙ = join K
cdleme46fg.a A = Atoms K
Assertion cdleme46f2g2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q K HL W H Q A ¬ Q ˙ W P A ¬ P ˙ W Q P S A ¬ S ˙ W ¬ S ˙ Q ˙ P

Proof

Step Hyp Ref Expression
1 cdleme46fg.j ˙ = join K
2 cdleme46fg.a A = Atoms K
3 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q K HL W H
4 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q Q A ¬ Q ˙ W
5 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q P A ¬ P ˙ W
6 3 4 5 3jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q K HL W H Q A ¬ Q ˙ W P A ¬ P ˙ W
7 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q P Q
8 7 necomd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q Q P
9 simp2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q S A ¬ S ˙ W
10 8 9 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q Q P S A ¬ S ˙ W
11 simpl1l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W K HL
12 simpl2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W P A
13 simpl3l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W Q A
14 1 2 hlatjcom K HL P A Q A P ˙ Q = Q ˙ P
15 11 12 13 14 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W P ˙ Q = Q ˙ P
16 15 breq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W S ˙ P ˙ Q S ˙ Q ˙ P
17 16 notbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q ¬ S ˙ Q ˙ P
18 17 biimp3a K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q ¬ S ˙ Q ˙ P
19 6 10 18 3jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q K HL W H Q A ¬ Q ˙ W P A ¬ P ˙ W Q P S A ¬ S ˙ W ¬ S ˙ Q ˙ P