Theorem orcs 889

Description: Deduction eliminating disjunct. Notational convention: We sometimes suffix with "s" the label of an inference that manipulates an antecedent, leaving the consequent unchanged. The "s" means that the inference eliminates the need for a syllogism (syl 18) -type inference in a proof. (Contributed by NM, 21-Jun-1994.)

Hypothesis

Ref	Expression
orcs.1	⊢ ((𝜑 ∨ 𝜓) → 𝜒)

Assertion

Ref	Expression
orcs	⊢ (𝜑 → 𝜒)

Proof of Theorem orcs

Step	Hyp	Ref	Expression
1		orc 881	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓))
2		orcs.1	. 2 ⊢ ((𝜑 ∨ 𝜓) → 𝜒)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → 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:  olcs  890  norasslem2  1565  ifor  4540  tppreqb  4771  frxp  8128  mndifsplit  22864  maducoeval2  22868  leibpilem2  27186  leibpi  27187  3o1cs  32946  3o2cs  32947  elrgspnlem2  33691  poimirlem31  38408  tsan2  38898  frege114d  44606  ntrneiel2  44934  nnfoctbdjlem  47291  homf0  49943