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:  elprn1  4613  disjxiun  5102  poxp2  8127  poxp3  8134  nnaordex2  8613  fpwwe2lem12  10615  fzone1  13804  chnub  18668  evlslem3  22191  psdmul  22289  plngcplem  29015  ccatws1f1o  33184  0ringsubrg  33484  drngidl  33657  mxidlmaxv  33668  mxidlprm  33670  rprmasso2  33733  1arithidom  33744  zringidom  33758  fldext2chn  34035  ordprcon  35393  aks6d1c2p2  42748  aks6d1c5  42768  chnerlem1  47456