Theorem olcnd 884

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 871	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
4	1, 3	mt3d 148	1 ⊢ (𝜑 → 𝜓)

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

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 209  df-or 855

This theorem is referenced by:  orcnd  885  ecase23d  1482  elprn2  4586  1sdom2dom  9158  finnzfsuppd  9280  fzone1  13734  tdeglem4  26046  ltonold  28273  xnn0nn0d  32866  ccatws1f1o  33032  mxidlirred  33557  dflring3  33590  dflring4  33591  fldextrspundgdvdslem  33874  fldext2rspun  33876  zarclssn  34067  eulerpartlemgvv  34570  lcmineqlem23  42549  chnerlem1  47339