Metamath Proof Explorer


Theorem cdlemednuN

Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma. D represents s_2. (Contributed by NM, 18-Nov-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemeda.l ˙=K
cdlemeda.j ˙=joinK
cdlemeda.m ˙=meetK
cdlemeda.a A=AtomsK
cdlemeda.h H=LHypK
cdlemeda.d D=R˙S˙W
cdlemednu.u U=P˙Q˙W
Assertion cdlemednuN KHLWHPAQARA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QDU

Proof

Step Hyp Ref Expression
1 cdlemeda.l ˙=K
2 cdlemeda.j ˙=joinK
3 cdlemeda.m ˙=meetK
4 cdlemeda.a A=AtomsK
5 cdlemeda.h H=LHypK
6 cdlemeda.d D=R˙S˙W
7 cdlemednu.u U=P˙Q˙W
8 1 2 3 4 5 6 cdlemednpq KHLWHPAQARA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙Q¬D˙P˙Q
9 simp1l KHLWHPAQARA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QKHL
10 simp1r KHLWHPAQARA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QWH
11 simp21 KHLWHPAQARA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QPA
12 simp22 KHLWHPAQARA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QQA
13 1 2 3 4 5 7 cdlemeulpq KHLWHPAQAU˙P˙Q
14 9 10 11 12 13 syl22anc KHLWHPAQARA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QU˙P˙Q
15 breq1 D=UD˙P˙QU˙P˙Q
16 14 15 syl5ibrcom KHLWHPAQARA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QD=UD˙P˙Q
17 16 necon3bd KHLWHPAQARA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙Q¬D˙P˙QDU
18 8 17 mpd KHLWHPAQARA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QDU