Theorem olci 406

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 391	1 |- ( ps \/ ph )

Syntax hints:   -. wn 3   \/ wo 383

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 197  df-or 385

This theorem is referenced by:  falortru  1512  sucidg  5803  kmlem2  8973  sornom  9099  leid  10133  pnf0xnn0  11370  xrleid  11983  xmul01  12097  bcn1  13100  odd2np1lem  15064  lcm0val  15307  lcmfunsnlem2lem1  15351  lcmfunsnlem2  15353  coprmprod  15375  coprmproddvdslem  15376  prmrec  15626  sratset  19184  srads  19186  m2detleib  20437  zclmncvs  22948  itg0  23546  itgz  23547  coemullem  24006  ftalem5  24803  chp1  24893  prmorcht  24904  pclogsum  24940  logexprlim  24950  bpos1  25008  pntpbnd1  25275  axlowdimlem16  25837  usgrexmpldifpr  26150  cusgrsizeindb1  26346  pthdlem2  26664  clwwlksn0  26907  ex-or  27278  plymulx0  30624  bj-0eltag  32966  bj-inftyexpidisj  33097  mblfinlem2  33447  volsupnfl  33454  ifpdfor  37809  ifpim1  37813  ifpnot  37814  ifpid2  37815  ifpim2  37816  ifpim1g  37846  ifpbi1b  37848  icccncfext  40100  fourierdlem103  40426  fourierdlem104  40427  etransclem24  40475  etransclem35  40486  abnotataxb  41083  dandysum2p2e4  41165  sbgoldbo  41675  zlmodzxzldeplem  42287  aacllem  42547