MPE Home 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 206  df-or 845
This theorem is referenced by:  0nn0  12349  fsum00  15609  pcfac  16697  mndifsplit  21891  bposlem2  26539  axcgrid  27573  3o2cs  31101  3o3cs  31102  fprodex01  31426  indsumin  32288  fsum2dsub  32887  finxpreclem2  35674  itg2addnclem  35941  tsan3  36414  ecexALTV  36605  cnvepimaex  36610  xrninxpex  36669  disjimxrn  37024
  Copyright terms: Public domain W3C validator