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  1503  ecase23d  1504  elprn2  4613  1sdom2dom  9273  finnzfsuppd  9392  fzone1  13946  tdeglem4  26408  ppinprm  27509  ltonold  28677  symquadprlnglem  29195  tgaaddcpbllem1  29379  tgaaddcpbl  29382  tgaaddcpbl2  29383  angmgmaddeu1  29409  angmgmaddcpbl  29420  tgextamirn  33097  tgextancd  33098  tgextamirnhl  33102  tgaasncol  33110  xnn0nn0d  33434  ccatws1f1o  33584  mxidlirred  34067  dflring3  34099  dflring4  34100  fldextrspundgdvdslem  34382  fldext2rspun  34384  zarclssn  34575  eulerpartlemgvv  35078  dfac16  35846  lcmineqlem23  43293  chnerlem1  48097