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  4596  disjxiun  5083  poxp2  8086  poxp3  8093  nnaordex2  8568  fpwwe2lem12  10556  fzone1  13730  chnub  18579  evlslem3  22068  psdmul  22142  ccatws1f1o  33026  0ringsubrg  33327  drngidl  33508  mxidlmaxv  33543  mxidlprm  33545  rprmasso2  33601  1arithidom  33612  zringidom  33626  fldext2chn  33888  aks6d1c2p2  42572  aks6d1c5  42592  chnerlem1  47328