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  11906  fsum00  15147  pcfac  16229  mndifsplit  21239  bposlem2  25855  axcgrid  26696  3o2cs  30222  3o3cs  30223  fprodex01  30536  indsumin  31276  fsum2dsub  31873  finxpreclem2  34665  itg2addnclem  34937  tsan3  35415  ecexALTV  35582  cnvepimaex  35587  xrninxpex  35636  disjimxrn  35973