Metamath Proof Explorer

Theorem cdlemg22

Description: cdlemg21 with ( FP ) =/= P condition removed. (Contributed by NM, 23-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)$
Assertion cdlemg22

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 simpl11
9 simpl12
10 simpl13
11 simpl21
12 simpl22
13 simpr
14 1 2 3 4 5 6 7 cdlemg14f
15 8 9 10 11 12 13 14 syl123anc
16 simpl1
17 simpl21
18 simpl22
19 17 18 jca
20 simpl23
21 simpr
22 simpl31
23 simpl32
24 simpl33
25 1 2 3 4 5 6 7 cdlemg21
26 16 19 20 21 22 23 24 25 syl133anc
27 15 26 pm2.61dane