Metamath Proof Explorer

Theorem cdlemg34

Description: Use cdlemg33 to eliminate z from cdlemg29 . TODO: Fix comment. (Contributed by NM, 31-May-2013)

Ref Expression
Hypotheses cdlemg12.l
cdlemg12.j
cdlemg12.m
cdlemg12.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemg12.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemg12.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemg12b.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdlemg31.n
cdlemg33.o
Assertion cdlemg34

Proof

Step Hyp Ref Expression
1 cdlemg12.l
2 cdlemg12.j
3 cdlemg12.m
4 cdlemg12.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 cdlemg12.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 cdlemg12.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
7 cdlemg12b.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
8 cdlemg31.n
9 cdlemg33.o
10 1 2 3 4 5 6 7 8 9 cdlemg33
11 simp11
12 simp121
13 simp2
14 simp3l
15 13 14 jca
16 simp122
17 simp3r1
18 simp3r2
19 17 18 jca
20 simp3r3
21 simp131
22 simp132
23 21 22 jca
24 1 2 3 4 5 6 7 8 9 cdlemg29
25 11 12 15 16 19 20 23 24 syl133anc
26 25 rexlimdv3a
27 10 26 mpd