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  1409  sucidg  4956  kmlem2  8527  sornom  8653  leid  9676  xrleid  11352  xmul01  11455  bcn1  12355  odd2np1lem  13900  prmrec  14295  sratset  17613  srads  17615  m2detleib  18900  itg0  21921  itgz  21922  coemullem  22381  ftalem5  23078  chp1  23169  prmorcht  23180  pclogsum  23218  logexprlim  23228  bpos1  23286  pntpbnd1  23499  axlowdimlem16  23936  usgraexmpldifpr  24076  cusgrasizeindb1  24147  vdgrf  24574  ex-or  24819  plymulx0  28144  mblfinlem2  29629  volsupnfl  29636  lcm0val  30800  icccncfext  31226  fourierdlem103  31510  fourierdlem104  31511  abnotataxb  31579  dandysum2p2e4  31637  zlmodzxzldeplem  32180  bj-0eltag  33617  bj-inftyexpidisj  33685
  Copyright terms: Public domain W3C validator