Theorem olcs 883

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

Syntax hints:   → wi 4   ∨ wo 854

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 209  df-or 855

This theorem is referenced by:  0nn0  12447  fsum00  15756  pcfac  16865  mndifsplit  22622  bposlem2  27269  axcgrid  29005  3o2cs  32551  3o3cs  32552  fprodex01  32919  indsumin  32942  fsum2dsub  34801  finxpreclem2  37765  itg2addnclem  38051  tsan3  38523  xrninxpex  38797  disjimxrn  39229