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  4610  poxp2  8095  poxp3  8102  nnaordex2  8577  fpwwe2lem12  10565  fzone1  13712  chnub  18557  evlslem3  22047  psdmul  22121  ccatws1f1o  33043  0ringsubrg  33344  drngidl  33525  mxidlmaxv  33560  mxidlprm  33562  rprmasso2  33618  1arithidom  33629  zringidom  33643  fldext2chn  33905  aks6d1c2p2  42483  aks6d1c5  42503  chnerlem1  47234