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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 860

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 861

This theorem is used by:  orcnd  891  ecase13d  1501  ecase23d  1502  elprn2  4617  1sdom2dom  9212  finnzfsuppd  9331  fzone1  13820  tdeglem4  26228  ltonold  28465  symquadprlnglem  28981  xnn0nn0d  33128  ccatws1f1o  33280  mxidlirred  33764  dflring3  33796  dflring4  33797  fldextrspundgdvdslem  34079  fldext2rspun  34081  zarclssn  34272  eulerpartlemgvv  34775  lcmineqlem23  42846  chnerlem1  47626