Theorem orcnd 884

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

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

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 208  df-or 854

This theorem is referenced by:  elprn1  4590  disjxiun  5076  poxp2  8090  poxp3  8097  nnaordex2  8572  fpwwe2lem12  10563  fzone1  13737  chnub  18586  evlslem3  22063  psdmul  22161  ccatws1f1o  33037  0ringsubrg  33339  drngidl  33523  mxidlmaxv  33558  mxidlprm  33560  rprmasso2  33616  1arithidom  33627  zringidom  33641  fldext2chn  33919  aks6d1c2p2  42611  aks6d1c5  42631  chnerlem1  47334