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  4612  disjxiun  5100  poxp2  8144  poxp3  8151  nnaordex2  8632  fpwwe2lem12  10708  fzone1  13899  chnub  18776  drngidl  21519  evlslem3  22369  psdmul  22467  plngcplem  29245  plngmiropp  29254  prlngin0  29404  prlngpln  29405  prlnghpg  29406  ccatws1f1o  33496  0ringsubrg  33794  mxidlmaxv  33975  mxidlprm  33977  rprmasso2  34040  1arithidom  34051  zringidom  34065  fldext2chn  34342  ordprcon  35696  aks6d1c2p2  43137  aks6d1c5  43157  sumnnodd  46586  chnerlem1  47836