Metamath Proof Explorer


Theorem cnfn2dd

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 ) )

Proof

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 ) )