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  4612  1sdom2dom  9245  finnzfsuppd  9365  fzone1  13919  tdeglem4  26378  ppinprm  27479  ltonold  28647  symquadprlnglem  29165  tgaaddcpbllem1  29349  tgaaddcpbl  29352  tgaaddcpbl2  29353  angmgmaddeu1  29379  angmgmaddcpbl  29390  tgextamirn  33067  tgextancd  33068  tgextamirnhl  33072  tgaasncol  33080  xnn0nn0d  33406  ccatws1f1o  33556  mxidlirred  34039  dflring3  34071  dflring4  34072  fldextrspundgdvdslem  34354  fldext2rspun  34356  zarclssn  34547  eulerpartlemgvv  35050  lcmineqlem23  43144  chnerlem1  47935