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  1468  sucidg  5518  kmlem2  8583  sornom  8709  leid  9731  xrleid  11451  xmul01  11555  bcn1  12499  odd2np1lem  14357  lcm0val  14551  lcmfunsnlem2lem1  14604  lcmfunsnlem2  14606  coprmprod  14671  coprmproddvdslem  14672  prmrec  14859  sratset  18400  srads  18402  m2detleib  19648  itg0  22729  itgz  22730  coemullem  23196  ftalem5  23993  ftalem5OLD  23995  chp1  24086  prmorcht  24097  pclogsum  24135  logexprlim  24145  bpos1  24203  pntpbnd1  24416  axlowdimlem16  24979  usgraexmpldifpr  25119  cusgrasizeindb1  25191  vdgrf  25618  ex-or  25863  plymulx0  29438  bj-0eltag  31534  bj-inftyexpidisj  31610  mblfinlem2  31898  volsupnfl  31905  ifpdfor  36034  ifpim1  36038  ifpnot  36039  ifpid2  36040  ifpim2  36041  ifpim1g  36071  ifpbi1b  36073  icccncfext  37591  fourierdlem103  37899  fourierdlem104  37900  etransclem24  37949  etransclem35  37960  abnotataxb  38223  dandysum2p2e4  38305  zlmodzxzldeplem  39597  aacllem  39846