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 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