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  12537  fsum00  15876  pcfac  16984  mndifsplit  22830  bposlem2  27486  axcgrid  29303  3o2cs  32847  3o3cs  32848  fprodex01  33206  indsumin  33218  fsum2dsub  35026  finxpreclem2  38077  itg2addnclem  38363  tsan3  38833  xrninxpex  39107  disjimxrn  39539