Metamath Proof Explorer


Theorem cdlemg16zz

Description: Eliminate P =/= Q from cdlemg16z . TODO: Use this only if needed. (Contributed by NM, 26-May-2013)

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 cdlemg16zz K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ 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 id P = Q P = Q
9 2fveq3 P = Q F G P = F G Q
10 8 9 oveq12d P = Q P ˙ F G P = Q ˙ F G Q
11 10 oveq1d P = Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
12 11 adantl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P = Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
13 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P Q K HL W H
14 simpl21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P Q P A ¬ P ˙ W
15 simpl22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P Q Q A ¬ Q ˙ W
16 simpl23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P Q F T
17 simpl31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P Q G T
18 simpr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P Q P Q
19 simpl32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P Q ¬ R F ˙ P ˙ Q
20 simpl33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P Q ¬ R G ˙ P ˙ Q
21 1 2 3 4 5 6 7 cdlemg16z 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 P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
22 13 14 15 16 17 18 19 20 21 syl332anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
23 12 22 pm2.61dane K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W