Theorem olcnd 891

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

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

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 862

This theorem is used by:  orcnd  892  ecase13d  1502  ecase23d  1503  elprn2  4616  1sdom2dom  9227  finnzfsuppd  9346  fzone1  13842  tdeglem4  26287  ppinprm  27386  ltonold  28524  symquadprlnglem  29042  tgaaddcpbllem1  29226  tgaaddcpbl  29229  tgaaddcpbl2  29230  angmndaddeu1  29252  angmndaddcpbl  29263  xnn0nn0d  33230  ccatws1f1o  33380  mxidlirred  33862  dflring3  33894  dflring4  33895  fldextrspundgdvdslem  34177  fldext2rspun  34179  zarclssn  34370  eulerpartlemgvv  34874  lcmineqlem23  42904  chnerlem1  47697