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

This theorem is referenced by:  0nn0  12568  fsum00  15846  pcfac  16946  mndifsplit  22663  bposlem2  27347  axcgrid  28949  3o2cs  32491  3o3cs  32492  fprodex01  32829  indsumin  33986  fsum2dsub  34584  finxpreclem2  37356  itg2addnclem  37631  tsan3  38103  ecexALTV  38287  cnvepimaex  38292  xrninxpex  38350  disjimxrn  38705