# Metamath Proof Explorer

## Theorem cdlemd5

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 30-May-2012)

Ref Expression
Hypotheses cdlemd4.l
cdlemd4.j
cdlemd4.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemd4.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemd4.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
Assertion cdlemd5

### Proof

Step Hyp Ref Expression
1 cdlemd4.l
2 cdlemd4.j
3 cdlemd4.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
4 cdlemd4.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
5 cdlemd4.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
6 fveq2 ${⊢}{R}={P}\to {F}\left({R}\right)={F}\left({P}\right)$
7 fveq2 ${⊢}{R}={P}\to {G}\left({R}\right)={G}\left({P}\right)$
8 6 7 eqeq12d ${⊢}{R}={P}\to \left({F}\left({R}\right)={G}\left({R}\right)↔{F}\left({P}\right)={G}\left({P}\right)\right)$
9 simpll1
10 simpl21
12 simpl22
14 simp23
16 simplr
17 simpr
18 15 16 17 3jca
19 simpll3
20 1 2 3 4 5 cdlemd4
21 9 11 13 18 19 20 syl131anc
22 simpl3l
23 8 21 22 pm2.61ne
24 simpl1
25 simpl21
26 simpl22
27 simpl23
28 simpr
29 27 28 jca
30 simpl3
31 1 2 3 4 5 cdlemd2
32 24 25 26 29 30 31 syl131anc
33 23 32 pm2.61dan