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  4611  disjxiun  5099  poxp2  8160  poxp3  8167  nnaordex2  8648  fpwwe2lem12  10727  fzone1  13919  chnub  18796  drngidl  21539  evlslem3  22389  psdmul  22487  plngcplem  29263  plngmiropp  29272  prlngin0  29422  prlngpln  29423  prlnghpg  29424  ccatws1f1o  33556  0ringsubrg  33854  mxidlmaxv  34035  mxidlprm  34037  rprmasso2  34100  1arithidom  34111  zringidom  34125  fldext2chn  34402  ordprcon  35757  aks6d1c2p2  43212  aks6d1c5  43232  sumnnodd  46684  chnerlem1  47934