Theorem olcs 875

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

Syntax hints:   → wi 4   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  0nn0  12487  fsum00  15744  pcfac  16832  mndifsplit  22138  bposlem2  26788  axcgrid  28174  3o2cs  31704  3o3cs  31705  fprodex01  32031  indsumin  33020  fsum2dsub  33619  finxpreclem2  36271  itg2addnclem  36539  tsan3  37011  ecexALTV  37200  cnvepimaex  37205  xrninxpex  37264  disjimxrn  37619