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

Theorem olci 381
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 366 1  |-  ( ps  \/  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    \/ wo 358
This theorem is referenced by:  falortru  1348  sucidg  4600  kmlem2  7964  sornom  8090  leid  9102  xrleid  10675  xmul01  10778  bcn1  11531  odd2np1lem  12834  prmrec  13217  sratset  16182  srads  16184  itg0  19538  itgz  19539  coemullem  20035  ftalem5  20726  chp1  20817  prmorcht  20828  pclogsum  20866  logexprlim  20876  bpos1  20934  pntpbnd1  21147  usgraexmpldifpr  21285  cusgrasizeindb1  21346  vdgrf  21517  ex-or  21577  axlowdimlem16  25610  volsupnfl  25956  abnotataxb  27553  dandysum2p2e4  27611
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360
  Copyright terms: Public domain W3C validator