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  4603  poxp2  8079  poxp3  8086  nnaordex2  8560  fpwwe2lem12  10540  fzone1  13686  chnub  18530  evlslem3  22016  psdmul  22082  ccatws1f1o  32939  0ringsubrg  33225  drngidl  33405  mxidlmaxv  33440  mxidlprm  33442  rprmasso2  33498  1arithidom  33509  zringidom  33523  fldext2chn  33762  aks6d1c2p2  42233  aks6d1c5  42253  chnerlem1  47005