Metamath Proof Explorer


Theorem olcnd

Description: A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017) (Proof shortened by Wolf Lammen, 13-Apr-2024)

Ref Expression
Hypotheses olcnd.1
|- ( ph -> ( ps \/ ch ) )
olcnd.2
|- ( ph -> -. ch )
Assertion olcnd
|- ( ph -> ps )

Proof

Step Hyp Ref Expression
1 olcnd.1
 |-  ( ph -> ( ps \/ ch ) )
2 olcnd.2
 |-  ( ph -> -. ch )
3 1 ord
 |-  ( ph -> ( -. ps -> ch ) )
4 2 3 mt3d
 |-  ( ph -> ps )