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  4615  disjxiun  5104  poxp2  8145  poxp3  8152  nnaordex2  8631  fpwwe2lem12  10655  fzone1  13844  chnub  18716  drngidl  21454  evlslem3  22302  psdmul  22400  plngcplem  29150  plngmiropp  29159  prlngin0  29309  prlngpln  29310  prlnghpg  29311  ccatws1f1o  33401  0ringsubrg  33699  mxidlmaxv  33879  mxidlprm  33881  rprmasso2  33944  1arithidom  33955  zringidom  33969  fldext2chn  34246  ordprcon  35600  aks6d1c2p2  42993  aks6d1c5  43013  chnerlem1  47718