Theorem orcnd 891

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

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

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 210  df-or 861

This theorem is referenced by:  ecase33d  1504  elprn1  4618  disjxiun  5107  poxp2  8140  poxp3  8147  nnaordex2  8626  fpwwe2lem12  10628  fzone1  13815  chnub  18679  drngidl  21366  evlslem3  22212  psdmul  22310  plngcplem  29045  plngmiropp  29054  prlngin0  29172  prlngpln  29173  prlnghpg  29174  ccatws1f1o  33249  0ringsubrg  33549  mxidlmaxv  33729  mxidlprm  33731  rprmasso2  33794  1arithidom  33805  zringidom  33819  fldext2chn  34096  ordprcon  35456  aks6d1c2p2  42864  aks6d1c5  42884  chnerlem1  47578