Theorem olcnd 886

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

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

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 857

This theorem is referenced by:  orcnd  887  ecase23d  1484  elprn2  4601  1sdom2dom  9183  finnzfsuppd  9305  fzone1  13776  tdeglem4  26089  ltonold  28320  xnn0nn0d  32913  ccatws1f1o  33079  mxidlirred  33604  dflring3  33637  dflring4  33638  fldextrspundgdvdslem  33921  fldext2rspun  33923  zarclssn  34114  eulerpartlemgvv  34617  lcmineqlem23  42606  chnerlem1  47396