Description: Create an atom under a co-atom. Part of proof of Lemma B in Crawley p. 112. (Contributed by NM, 23-May-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lhpat.l | |
|
lhpat.j | |
||
lhpat.m | |
||
lhpat.a | |
||
lhpat.h | |
||
Assertion | lhpat | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lhpat.l | |
|
2 | lhpat.j | |
|
3 | lhpat.m | |
|
4 | lhpat.a | |
|
5 | lhpat.h | |
|
6 | simp1l | |
|
7 | simp2l | |
|
8 | simp3l | |
|
9 | simp1r | |
|
10 | eqid | |
|
11 | 10 5 | lhpbase | |
12 | 9 11 | syl | |
13 | simp3r | |
|
14 | eqid | |
|
15 | eqid | |
|
16 | 14 15 5 | lhp1cvr | |
17 | 16 | 3ad2ant1 | |
18 | simp2r | |
|
19 | 10 1 2 3 14 15 4 | 1cvrat | |
20 | 6 7 8 12 13 17 18 19 | syl133anc | |