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 ( 𝜑 → ( 𝜓𝜒 ) )
olcnd.2 ( 𝜑 → ¬ 𝜒 )
Assertion olcnd ( 𝜑𝜓 )

Proof

Step Hyp Ref Expression
1 olcnd.1 ( 𝜑 → ( 𝜓𝜒 ) )
2 olcnd.2 ( 𝜑 → ¬ 𝜒 )
3 1 ord ( 𝜑 → ( ¬ 𝜓𝜒 ) )
4 2 3 mt3d ( 𝜑𝜓 )