Theorem orcnd 892

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  ecase33d  1504  elprn1  4622  disjxiun  5111  poxp2  8148  poxp3  8155  nnaordex2  8634  fpwwe2lem12  10645  fzone1  13832  chnub  18703  drngidl  21422  evlslem3  22268  psdmul  22366  plngcplem  29104  plngmiropp  29113  prlngin0  29231  prlngpln  29232  prlnghpg  29233  ccatws1f1o  33304  0ringsubrg  33602  mxidlmaxv  33782  mxidlprm  33784  rprmasso2  33847  1arithidom  33858  zringidom  33872  fldext2chn  34149  ordprcon  35503  aks6d1c2p2  42927  aks6d1c5  42947  chnerlem1  47639