Theorem olci 393

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

Step	Hyp	Ref	Expression
1		orci.1	. . 3 |- ph
2	1	a1i 11	. 2 |- ( -. ps -> ph )
3	2	orri 378	1 |- ( ps \/ ph )

Syntax hints:   -. wn 3   \/ wo 370

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 189  df-or 372

This theorem is referenced by:  falortru  1472  sucidg  5501  kmlem2  8581  sornom  8707  leid  9729  xrleid  11449  xmul01  11553  bcn1  12498  odd2np1lem  14364  lcm0val  14558  lcmfunsnlem2lem1  14611  lcmfunsnlem2  14613  coprmprod  14678  coprmproddvdslem  14679  prmrec  14866  sratset  18407  srads  18409  m2detleib  19656  itg0  22737  itgz  22738  coemullem  23204  ftalem5  24001  ftalem5OLD  24003  chp1  24094  prmorcht  24105  pclogsum  24143  logexprlim  24153  bpos1  24211  pntpbnd1  24424  axlowdimlem16  24987  usgraexmpldifpr  25127  cusgrasizeindb1  25199  vdgrf  25626  ex-or  25871  plymulx0  29436  bj-0eltag  31572  bj-inftyexpidisj  31652  mblfinlem2  31978  volsupnfl  31985  ifpdfor  36108  ifpim1  36112  ifpnot  36113  ifpid2  36114  ifpim2  36115  ifpim1g  36145  ifpbi1b  36147  icccncfext  37765  fourierdlem103  38073  fourierdlem104  38074  etransclem24  38123  etransclem35  38134  abnotataxb  38504  dandysum2p2e4  38586  pnf0xnn0  39078  cusgrsizeindb1  39511  zlmodzxzldeplem  40344  aacllem  40593