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

Theorem olcs 875
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 871 . 2 ((𝜓𝜑) → 𝜒)
32orcs 874 1 (𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 846
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 847
This theorem is referenced by:  0nn0  12483  fsum00  15740  pcfac  16828  mndifsplit  22120  bposlem2  26768  axcgrid  28154  3o2cs  31682  3o3cs  31683  fprodex01  32009  indsumin  32958  fsum2dsub  33557  finxpreclem2  36209  itg2addnclem  36477  tsan3  36949  ecexALTV  37138  cnvepimaex  37143  xrninxpex  37202  disjimxrn  37557
  Copyright terms: Public domain W3C validator