Theorem olcs 876

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

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  0nn0  12539  fsum00  15831  pcfac  16933  mndifsplit  22658  bposlem2  27344  axcgrid  28946  3o2cs  32491  3o3cs  32492  fprodex01  32832  indsumin  34003  fsum2dsub  34601  finxpreclem2  37373  itg2addnclem  37658  tsan3  38130  ecexALTV  38313  cnvepimaex  38318  xrninxpex  38376  disjimxrn  38731