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

Assertion

Ref	Expression
olci

Proof of Theorem olci

Step	Hyp	Ref	Expression
1		orci.1	. . 3
2	1	a1i 11	. 2
3	2	orri 376	1

Syntax hints:  -.wn 3  \/wo 368

This theorem is referenced by:  falortru  1425  sucidg  4961  kmlem2  8552  sornom  8678  leid  9701  xrleid  11385  xmul01  11488  bcn1  12391  odd2np1lem  14045  prmrec  14440  sratset  17830  srads  17832  m2detleib  19133  itg0  22186  itgz  22187  coemullem  22647  ftalem5  23350  chp1  23441  prmorcht  23452  pclogsum  23490  logexprlim  23500  bpos1  23558  pntpbnd1  23771  axlowdimlem16  24260  usgraexmpldifpr  24400  cusgrasizeindb1  24471  vdgrf  24898  ex-or  25142  plymulx0  28504  mblfinlem2  30052  volsupnfl  30059  lcm0val  31200  icccncfext  31690  fourierdlem103  31992  fourierdlem104  31993  etransclem24  32041  etransclem35  32052  abnotataxb  32112  dandysum2p2e4  32170  zlmodzxzldeplem  33099  aacllem  33216  bj-0eltag  34536  bj-inftyexpidisj  34613  bj-ifid2  37711  bj-ifim1  37712  bj-ifim2  37713  bj-ifim1g  37714  bj-ifnot  37717  bj-ifdfor  37722

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