Theorem olcnd 890

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

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

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 210  df-or 861

This theorem is referenced by:  orcnd  891  ecase13d  1500  ecase23d  1501  elprn2  4617  1sdom2dom  9213  finnzfsuppd  9332  fzone1  13812  tdeglem4  26196  ltonold  28430  xnn0nn0d  33083  ccatws1f1o  33237  mxidlirred  33721  dflring3  33753  dflring4  33754  fldextrspundgdvdslem  34036  fldext2rspun  34038  zarclssn  34229  eulerpartlemgvv  34732  lcmineqlem23  42764  chnerlem1  47546