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

This theorem is referenced by:  0nn0  11913  fsum00  15153  pcfac  16235  mndifsplit  21245  bposlem2  25861  axcgrid  26702  3o2cs  30228  3o3cs  30229  fprodex01  30541  indsumin  31281  fsum2dsub  31878  finxpreclem2  34674  itg2addnclem  34958  tsan3  35436  ecexALTV  35603  cnvepimaex  35608  xrninxpex  35657  disjimxrn  35994