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

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

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 187  df-or 370

This theorem is referenced by:  falortru  1437  sucidg  5490  kmlem2  8565  sornom  8691  leid  9713  xrleid  11411  xmul01  11514  bcn1  12437  odd2np1lem  14256  prmrec  14651  sratset  18152  srads  18154  m2detleib  19427  itg0  22480  itgz  22481  coemullem  22941  ftalem5  23733  chp1  23824  prmorcht  23835  pclogsum  23873  logexprlim  23883  bpos1  23941  pntpbnd1  24154  axlowdimlem16  24689  usgraexmpldifpr  24829  cusgrasizeindb1  24900  vdgrf  25327  ex-or  25572  plymulx0  29023  bj-0eltag  31114  bj-inftyexpidisj  31190  mblfinlem2  31437  volsupnfl  31444  ifpdfor  35568  ifpim1  35572  ifpnot  35573  ifpid2  35574  ifpim2  35575  ifpim1g  35605  ifpbi1b  35607  lcm0val  36061  icccncfext  37071  fourierdlem103  37373  fourierdlem104  37374  etransclem24  37422  etransclem35  37433  abnotataxb  37493  dandysum2p2e4  37551  zlmodzxzldeplem  38623  aacllem  38873