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

Theorem olci 380
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 10 . 2  |-  ( -. 
ps  ->  ph )
32orri 365 1  |-  ( ps  \/  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    \/ wo 357
This theorem is referenced by:  falortru  1332  sucidg  4470  kmlem2  7777  sornom  7903  leid  8916  xrleid  10484  xmul01  10587  bcn1  11325  odd2np1lem  12586  prmrec  12969  sratset  15936  srads  15938  itg0  19134  itgz  19135  coemullem  19631  ftalem5  20314  chp1  20405  prmorcht  20416  pclogsum  20454  logexprlim  20464  bpos1  20522  pntpbnd1  20735  ex-or  20808  axlowdimlem16  24585  pfsubkl  26047  stoweidlem38  27787  dandysum2p2e4  27943  usgraex3elv  28131  usgraexmpldifpr  28132
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 177  df-or 359
  Copyright terms: Public domain W3C validator