Theorem orcs 888

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 880	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓))
2		orcs.1	. 2 ⊢ ((𝜑 ∨ 𝜓) → 𝜒)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → 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:  olcs  889  norasslem2  1565  ifor  4543  tppreqb  4774  frxp  8123  mndifsplit  22774  maducoeval2  22778  leibpilem2  27084  leibpi  27085  3o1cs  32787  3o2cs  32788  elrgspnlem2  33541  poimirlem31  38280  tsan2  38769  frege114d  44464  ntrneiel2  44792  nnfoctbdjlem  47149  homf0  49764