Metamath Proof Explorer


Theorem cdlemg16ALTN

Description: This version of cdlemg16 uses cdlemg15a instead of cdlemg15 , in case cdlemg15 ends up not being needed. TODO: FIX COMMENT. (Contributed by NM, 6-May-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cdlemg12.l ˙ = K
2 cdlemg12.j ˙ = join K
3 cdlemg12.m ˙ = meet K
4 cdlemg12.a A = Atoms K
5 cdlemg12.h H = LHyp K
6 cdlemg12.t T = LTrn K W
7 cdlemg12b.r R = trL K W
8 simpl11 K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F = R G K HL
9 simpl12 K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F = R G W H
10 8 9 jca K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F = R G K HL W H
11 simpl21 K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F = R G P A ¬ P ˙ W
12 simpl22 K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F = R G Q A ¬ Q ˙ W
13 simpl13 K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F = R G F T G T
14 simpr K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F = R G R F = R G
15 simpl31 K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F = R G F G P ˙ F G Q P ˙ Q
16 1 2 3 4 5 6 7 cdlemg15a K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T R F = R G F G P ˙ F G Q P ˙ Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
17 10 11 12 13 14 15 16 syl312anc K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F = R G P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
18 simpl11 K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F R G K HL
19 simpl12 K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F R G W H
20 18 19 jca K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F R G K HL W H
21 simpl21 K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F R G P A ¬ P ˙ W
22 simpl22 K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F R G Q A ¬ Q ˙ W
23 simp13l K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F T
24 23 adantr K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F R G F T
25 simp13r K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q G T
26 25 adantr K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F R G G T
27 simpl23 K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F R G P Q
28 simpl32 K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F R G ¬ R F ˙ P ˙ Q
29 simpl33 K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F R G ¬ R G ˙ P ˙ Q
30 28 29 jca K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F R G ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q
31 simpr K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F R G R F R G
32 simpl31 K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F R G F G P ˙ F G Q P ˙ Q
33 1 2 3 4 5 6 7 cdlemg12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F R G F G P ˙ F G Q P ˙ Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
34 20 21 22 24 26 27 30 31 32 33 syl333anc K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F R G P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
35 17 34 pm2.61dane K HL W H F T G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W