Theorem orcnd 878

Description: A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)

Hypotheses

Ref	Expression
orcnd.1	⊢ (𝜑 → (𝜓 ∨ 𝜒))
orcnd.2	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
orcnd	⊢ (𝜑 → 𝜒)

Proof of Theorem orcnd

Step	Hyp	Ref	Expression
1		orcnd.1	. . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
2	1	orcomd 871	. 2 ⊢ (𝜑 → (𝜒 ∨ 𝜓))
3		orcnd.2	. 2 ⊢ (𝜑 → ¬ 𝜓)
4	2, 3	olcnd 877	1 ⊢ (𝜑 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-or 848

This theorem is referenced by:  elprn1  4608  poxp2  8085  poxp3  8092  nnaordex2  8567  fpwwe2lem12  10553  fzone1  13700  chnub  18545  evlslem3  22035  psdmul  22109  ccatws1f1o  33033  0ringsubrg  33333  drngidl  33514  mxidlmaxv  33549  mxidlprm  33551  rprmasso2  33607  1arithidom  33618  zringidom  33632  fldext2chn  33885  aks6d1c2p2  42369  aks6d1c5  42389  chnerlem1  47122