Theorem olcs 873

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 869	. 2 ⊢ ((𝜓 ∨ 𝜑) → 𝜒)
3	2	orcs 872	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4   ∨ wo 844

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 210  df-or 845

This theorem is referenced by:  0nn0  11949  fsum00  15201  pcfac  16290  mndifsplit  21336  bposlem2  25968  axcgrid  26809  3o2cs  30333  3o3cs  30334  fprodex01  30663  indsumin  31509  fsum2dsub  32106  finxpreclem2  35087  itg2addnclem  35388  tsan3  35861  ecexALTV  36028  cnvepimaex  36033  xrninxpex  36082  disjimxrn  36419