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  12547  fsum00  15889  pcfac  16997  mndifsplit  22864  bposlem2  27529  axcgrid  29381  3o2cs  32947  3o3cs  32948  fprodex01  33303  indsumin  33315  fsum2dsub  35123  finxpreclem2  38152  itg2addnclem  38428  tsan3  38899  xrninxpex  39173  disjimxrn  39605