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:  poxp2  8142  poxp3  8149  nnaordex2  8651  fpwwe2lem12  10656  evlslem3  22038  psdmul  22104  fzone1  32777  ccatws1f1o  32927  chnub  32992  0ringsubrg  33246  drngidl  33448  mxidlmaxv  33483  mxidlprm  33485  rprmasso2  33541  1arithidom  33552  zringidom  33566  fldext2chn  33762  aks6d1c2p2  42132  aks6d1c5  42152