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  1399  sucidg  4797  kmlem2  8320  sornom  8446  leid  9470  xrleid  11127  xmul01  11230  bcn1  12089  odd2np1lem  13591  prmrec  13983  sratset  17265  srads  17267  m2detleib  18437  itg0  21257  itgz  21258  coemullem  21717  ftalem5  22414  chp1  22505  prmorcht  22516  pclogsum  22554  logexprlim  22564  bpos1  22622  pntpbnd1  22835  axlowdimlem16  23203  usgraexmpldifpr  23318  cusgrasizeindb1  23379  vdgrf  23568  ex-or  23628  plymulx0  26948  mblfinlem2  28429  volsupnfl  28436  abnotataxb  29931  dandysum2p2e4  29989  zlmodzxzldeplem  31040  bj-0eltag  32471  bj-inftyexpidisj  32533