This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem orcnd

Description: A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017)

Ref Expression
Hypotheses orcnd.1 ⊢ φ → ψ ∨ χ
orcnd.2 ⊢ φ → ¬ ψ
Assertion orcnd ⊢ φ → χ

Proof

Step Hyp Ref Expression
1 orcnd.1 ⊢ φ → ψ ∨ χ
2 orcnd.2 ⊢ φ → ¬ ψ
3 1 orcomd ⊢ φ → χ ∨ ψ
4 3 2 olcnd ⊢ φ → χ