Metamath Proof Explorer


Theorem cdlemg38

Description: Use cdlemg37 to eliminate E. r e. A from cdlemg36 . TODO: Fix comment. (Contributed by NM, 31-May-2013)

Ref Expression
Hypotheses cdlemg35.l ˙ = K
cdlemg35.j ˙ = join K
cdlemg35.m ˙ = meet K
cdlemg35.a A = Atoms K
cdlemg35.h H = LHyp K
cdlemg35.t T = LTrn K W
cdlemg35.r R = trL K W
Assertion cdlemg38 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G P ˙ F G P ˙ W = Q ˙ F G Q ˙ W

Proof

Step Hyp Ref Expression
1 cdlemg35.l ˙ = K
2 cdlemg35.j ˙ = join K
3 cdlemg35.m ˙ = meet K
4 cdlemg35.a A = Atoms K
5 cdlemg35.h H = LHyp K
6 cdlemg35.t T = LTrn K W
7 cdlemg35.r R = trL K W
8 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
9 simpl2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r F T G T P Q
10 simpl3l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r F P P G P P
11 simpl3r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r R F R G
12 simpr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r r A ¬ r ˙ W P ˙ r = Q ˙ r
13 1 2 3 4 5 6 7 cdlemg36 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
14 8 9 10 11 12 13 syl113anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
15 simpl11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r K HL W H
16 simpl12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A ¬ P ˙ W
17 simpl13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r Q A ¬ Q ˙ W
18 simpl21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r F T
19 simpl22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r G T
20 simpl23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P Q
21 simpr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r
22 1 2 3 4 5 6 7 cdlemg37 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
23 15 16 17 18 19 20 21 22 syl133anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
24 14 23 pm2.61dan K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G P ˙ F G P ˙ W = Q ˙ F G Q ˙ W