Theorem olcnd 878

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

Hypotheses

Ref	Expression
olcnd.1	⊢ (𝜑 → (𝜓 ∨ 𝜒))
olcnd.2	⊢ (𝜑 → ¬ 𝜒)

Assertion

Ref	Expression
olcnd	⊢ (𝜑 → 𝜓)

Proof of Theorem olcnd

Step	Hyp	Ref	Expression
1		olcnd.2	. 2 ⊢ (𝜑 → ¬ 𝜒)
2		olcnd.1	. . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
3	2	ord 865	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
4	1, 3	mt3d 148	1 ⊢ (𝜑 → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-or 849

This theorem is referenced by:  orcnd  879  ecase23d  1476  elprn2  4610  1sdom2dom  9158  finnzfsuppd  9280  fzone1  13704  tdeglem4  26025  sltonold  28242  xnn0nn0d  32833  ccatws1f1o  33014  mxidlirred  33534  fldextrspundgdvdslem  33818  fldext2rspun  33820  zarclssn  34011  eulerpartlemgvv  34514  lcmineqlem23  42342  chnerlem1  47162