Description: A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cnfn2dd.1 | |- ( ph -> ( ps -> th ) ) |
|
cnfn2dd.2 | |- ( ph -> ( ps -> ( ch \/ -. th ) ) ) |
||
Assertion | cnfn2dd | |- ( ph -> ( ps -> ch ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnfn2dd.1 | |- ( ph -> ( ps -> th ) ) |
|
2 | cnfn2dd.2 | |- ( ph -> ( ps -> ( ch \/ -. th ) ) ) |
|
3 | notnot | |- ( th -> -. -. th ) |
|
4 | 1 3 | syl6 | |- ( ph -> ( ps -> -. -. th ) ) |
5 | 4 2 | cnf2dd | |- ( ph -> ( ps -> ch ) ) |