Theorem orcnd 889

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 882	. 2 ⊢ (𝜑 → (𝜒 ∨ 𝜓))
3		orcnd.2	. 2 ⊢ (𝜑 → ¬ 𝜓)
4	2, 3	olcnd 888	1 ⊢ (𝜑 → 𝜒)

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

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 209  df-or 859

This theorem is referenced by:  elprn1  4609  disjxiun  5096  poxp2  8118  poxp3  8125  nnaordex2  8604  fpwwe2lem12  10597  fzone1  13787  chnub  18637  evlslem3  22113  psdmul  22211  ccatws1f1o  33090  0ringsubrg  33393  drngidl  33580  mxidlmaxv  33617  mxidlprm  33619  rprmasso2  33683  1arithidom  33694  zringidom  33708  fldext2chn  33986  ordprcon  35347  aks6d1c2p2  42700  aks6d1c5  42720  chnerlem1  47422