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  1505  elprn1  4612  disjxiun  5103  poxp2  8187  poxp3  8194  nnaordex2  8676  fpwwe2lem12  10754  fzone1  13946  chnub  18825  drngidl  21569  evlslem3  22419  psdmul  22517  plngcplem  29293  plngmiropp  29302  prlngin0  29452  prlngpln  29453  prlnghpg  29454  ccatws1f1o  33584  0ringsubrg  33882  mxidlmaxv  34063  mxidlprm  34065  rprmasso2  34128  1arithidom  34139  zringidom  34153  fldext2chn  34430  ordprcon  35793  0elscott  35837  aks6d1c2p2  43361  aks6d1c5  43381  sumnnodd  46847  chnerlem1  48097  parhomne2  50959