# Metamath Proof Explorer

## Theorem cdlemg43

Description: Part of proof of Lemma G of Crawley p. 116, third line of third paragraph on p. 117. (Contributed by NM, 3-Jun-2013)

Ref Expression
Hypotheses cdlemg42.l
cdlemg42.j
cdlemg42.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemg42.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemg42.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemg42.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdlemg42.m
Assertion cdlemg43

### Proof

Step Hyp Ref Expression
1 cdlemg42.l
2 cdlemg42.j
3 cdlemg42.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
4 cdlemg42.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
5 cdlemg42.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
6 cdlemg42.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
7 cdlemg42.m
8 simp1
9 simp2l
10 simp31
11 simp2r
12 1 3 4 5 ltrnel
13 8 11 10 12 syl3anc
14 1 2 3 4 5 6 cdlemg42
15 1 2 7 3 4 5 6 cdlemc
16 8 9 10 13 14 15 syl131anc
17 1 2 7 3 4 5 6 trlval2
18 8 11 10 17 syl3anc
19 18 oveq2d
20 19 oveq2d
21 16 20 eqtr4d