Theorem orcnd 879

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

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

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 849

This theorem is referenced by:  elprn1  4595  disjxiun  5082  poxp2  8093  poxp3  8100  nnaordex2  8575  fpwwe2lem12  10565  fzone1  13739  chnub  18588  evlslem3  22058  psdmul  22132  ccatws1f1o  33011  0ringsubrg  33312  drngidl  33493  mxidlmaxv  33528  mxidlprm  33530  rprmasso2  33586  1arithidom  33597  zringidom  33611  fldext2chn  33872  aks6d1c2p2  42558  aks6d1c5  42578  chnerlem1  47312