Theorem olcs 890

Description: Deduction eliminating disjunct. (Contributed by NM, 21-Jun-1994.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)

Hypothesis

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

Assertion

Ref	Expression
olcs	⊢ (𝜓 → 𝜒)

Proof of Theorem olcs

Step	Hyp	Ref	Expression
1		olcs.1	. . 3 ⊢ ((𝜑 ∨ 𝜓) → 𝜒)
2	1	orcoms 886	. 2 ⊢ ((𝜓 ∨ 𝜑) → 𝜒)
3	2	orcs 889	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:  0nn0  12602  fsum00  15945  pcfac  17057  mndifsplit  22931  bposlem2  27594  axcgrid  29476  3o2cs  33042  3o3cs  33043  fprodex01  33398  indsumin  33410  fsum2dsub  35219  finxpreclem2  38281  itg2addnclem  38557  tsan3  39043  xrninxpex  39317  disjimxrn  39749