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  9223  finnzfsuppd  9343  fzone1  13887  tdeglem4  26339  ppinprm  27442  ltonold  28580  symquadprlnglem  29098  tgaaddcpbllem1  29282  tgaaddcpbl  29285  tgaaddcpbl2  29286  angmgmaddeu1  29312  angmgmaddcpbl  29323  xnn0nn0d  33297  ccatws1f1o  33447  mxidlirred  33930  dflring3  33962  dflring4  33963  fldextrspundgdvdslem  34245  fldext2rspun  34247  zarclssn  34438  eulerpartlemgvv  34942  lcmineqlem23  43021  chnerlem1  47814