Theorem olcs 872

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

Syntax hints:   → wi 4   ∨ wo 843

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 844

This theorem is referenced by:  0nn0  12231  fsum00  15491  pcfac  16581  mndifsplit  21766  bposlem2  26414  axcgrid  27265  3o2cs  30792  3o3cs  30793  fprodex01  31118  indsumin  31969  fsum2dsub  32566  finxpreclem2  35540  itg2addnclem  35807  tsan3  36280  ecexALTV  36445  cnvepimaex  36450  xrninxpex  36499  disjimxrn  36836