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  4486  kmlem2  7793  sornom  7919  leid  8932  xrleid  10500  xmul01  10603  bcn1  11341  odd2np1lem  12602  prmrec  12985  sratset  15952  srads  15954  itg0  19150  itgz  19151  coemullem  19647  ftalem5  20330  chp1  20421  prmorcht  20432  pclogsum  20470  logexprlim  20480  bpos1  20538  pntpbnd1  20751  ex-or  20824  axlowdimlem16  24657  pfsubkl  26150  stoweidlem38  27890  dandysum2p2e4  28046  usgraex3elv  28265  usgraexmpldifpr  28266
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