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  4604  poxp2  8073  poxp3  8080  nnaordex2  8554  fpwwe2lem12  10533  fzone1  13684  chnub  18528  evlslem3  22016  psdmul  22082  ccatws1f1o  32930  0ringsubrg  33216  drngidl  33396  mxidlmaxv  33431  mxidlprm  33433  rprmasso2  33489  1arithidom  33500  zringidom  33514  fldext2chn  33739  aks6d1c2p2  42158  aks6d1c5  42178