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

Theorem olcs 409
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 403 . 2 ((𝜓𝜑) → 𝜒)
32orcs 408 1 (𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382
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 197  df-or 384
This theorem is referenced by:  0nn0  11345  fsum00  14574  pcfac  15650  mndifsplit  20490  bposlem2  25055  axcgrid  25841  3o2cs  29438  3o3cs  29439  fprodex01  29699  indsumin  30212  fsum2dsub  30813  finxpreclem2  33357  itg2addnclem  33591  tsan3  34080  xrninxpex  34292
  Copyright terms: Public domain W3C validator