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  4608  disjxiun  5099  poxp2  8162  poxp3  8169  nnaordex2  8651  fpwwe2lem12  10730  fzone1  13922  chnub  18801  drngidl  21544  evlslem3  22394  psdmul  22492  plngcplem  29268  plngmiropp  29277  prlngin0  29427  prlngpln  29428  prlnghpg  29429  ccatws1f1o  33560  0ringsubrg  33858  mxidlmaxv  34039  mxidlprm  34041  rprmasso2  34104  1arithidom  34115  zringidom  34129  fldext2chn  34406  ordprcon  35766  aks6d1c2p2  43262  aks6d1c5  43282  sumnnodd  46735  chnerlem1  47985  parhomne2  50847