Theorem orcs 875

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

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  olcs  876  norasslem2  1536  ifor  4530  tppreqb  4757  frxp  8056  mndifsplit  22549  maducoeval2  22553  leibpilem2  26876  leibpi  26877  3o1cs  32435  3o2cs  32436  elrgspnlem2  33205  poimirlem31  37690  tsan2  38181  frege114d  43790  ntrneiel2  44118  nnfoctbdjlem  46492  homf0  49040