Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  olcs Structured version   Visualization version   GIF version

Theorem olcs 873
 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
StepHypRef Expression
1 olcs.1 . . 3 ((𝜑𝜓) → 𝜒)
21orcoms 869 . 2 ((𝜓𝜑) → 𝜒)
32orcs 872 1 (𝜓𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 844 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 210  df-or 845 This theorem is referenced by:  0nn0  11949  fsum00  15201  pcfac  16290  mndifsplit  21336  bposlem2  25968  axcgrid  26809  3o2cs  30333  3o3cs  30334  fprodex01  30663  indsumin  31509  fsum2dsub  32106  finxpreclem2  35087  itg2addnclem  35388  tsan3  35861  ecexALTV  36028  cnvepimaex  36033  xrninxpex  36082  disjimxrn  36419
 Copyright terms: Public domain W3C validator