Description: Given two atoms not under the fiducial (reference) co-atom W , there is a third. Lemma B in Crawley p. 112. (Contributed by NM, 30-May-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemb2.l | |
|
cdlemb2.j | |
||
cdlemb2.a | |
||
cdlemb2.h | |
||
Assertion | cdlemb2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemb2.l | |
|
2 | cdlemb2.j | |
|
3 | cdlemb2.a | |
|
4 | cdlemb2.h | |
|
5 | simp1l | |
|
6 | simp2ll | |
|
7 | simp2rl | |
|
8 | simp1r | |
|
9 | eqid | |
|
10 | 9 4 | lhpbase | |
11 | 8 10 | syl | |
12 | simp3 | |
|
13 | eqid | |
|
14 | eqid | |
|
15 | 13 14 4 | lhp1cvr | |
16 | 15 | 3ad2ant1 | |
17 | simp2lr | |
|
18 | simp2rr | |
|
19 | 9 1 2 13 14 3 | cdlemb | |
20 | 5 6 7 11 12 16 17 18 19 | syl323anc | |