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  1564  ifor  4536  tppreqb  4764  frxp  8140  mndifsplit  22956  maducoeval2  22960  leibpilem2  27274  leibpi  27275  3o1cs  33106  3o2cs  33107  elrgspnlem2  33850  poimirlem31  38662  tsan2  39167  frege114d  44851  ntrneiel2  45179  nnfoctbdjlem  47558  homf0  50216