MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  olci Structured version   Unicode version

Theorem olci 391
Description: Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
Hypothesis
Ref Expression
orci.1  |-  ph
Assertion
Ref Expression
olci  |-  ( ps  \/  ph )

Proof of Theorem olci
StepHypRef Expression
1 orci.1 . . 3  |-  ph
21a1i 11 . 2  |-  ( -. 
ps  ->  ph )
32orri 376 1  |-  ( ps  \/  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    \/ wo 368
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 185  df-or 370
This theorem is referenced by:  falortru  1399  sucidg  4797  kmlem2  8320  sornom  8446  leid  9470  xrleid  11127  xmul01  11230  bcn1  12089  odd2np1lem  13591  prmrec  13983  sratset  17265  srads  17267  m2detleib  18437  itg0  21257  itgz  21258  coemullem  21717  ftalem5  22414  chp1  22505  prmorcht  22516  pclogsum  22554  logexprlim  22564  bpos1  22622  pntpbnd1  22835  axlowdimlem16  23203  usgraexmpldifpr  23318  cusgrasizeindb1  23379  vdgrf  23568  ex-or  23628  plymulx0  26948  mblfinlem2  28429  volsupnfl  28436  abnotataxb  29931  dandysum2p2e4  29989  zlmodzxzldeplem  31040  bj-0eltag  32471  bj-inftyexpidisj  32533
  Copyright terms: Public domain W3C validator