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

Theorem olci 382
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 367 1  |-  ( ps  \/  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    \/ wo 359
This theorem is referenced by:  falortru  1352  sucidg  4662  kmlem2  8036  sornom  8162  leid  9174  xrleid  10748  xmul01  10851  bcn1  11609  odd2np1lem  12912  prmrec  13295  sratset  16260  srads  16262  itg0  19674  itgz  19675  coemullem  20173  ftalem5  20864  chp1  20955  prmorcht  20966  pclogsum  21004  logexprlim  21014  bpos1  21072  pntpbnd1  21285  usgraexmpldifpr  21424  cusgrasizeindb1  21485  vdgrf  21674  ex-or  21734  axlowdimlem16  25901  mblfinlem2  26256  volsupnfl  26263  abnotataxb  27875  dandysum2p2e4  27933
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 179  df-or 361
  Copyright terms: Public domain W3C validator