Theorem olci 863

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 859	1 ⊢ (𝜓 ∨ 𝜑)

Syntax hints:  ¬ wn 3   ∨ wo 844

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 206  df-or 845

This theorem is referenced by:  falortru  1578  opthhausdorff  5431  sucidg  6344  kmlem2  9907  sornom  10033  leid  11071  pnf0xnn0  12312  xrleid  12885  xmul01  13001  bcn1  14027  odd2np1lem  16049  lcm0val  16299  lcmfunsnlem2lem1  16343  lcmfunsnlem2  16345  coprmprod  16366  coprmproddvdslem  16367  prmrec  16623  smndex2dnrinv  18554  sratsetOLD  20453  sradsOLD  20456  m2detleib  21780  zclmncvs  24312  itg0  24944  itgz  24945  coemullem  25411  ftalem5  26226  chp1  26316  prmorcht  26327  pclogsum  26363  logexprlim  26373  bpos1  26431  addsqnreup  26591  pntpbnd1  26734  axlowdimlem16  27325  usgrexmpldifpr  27625  cusgrsizeindb1  27817  pthdlem2  28136  ex-or  28785  plymulx0  32526  signstfvn  32548  bj-0eltag  35168  bj-inftyexpidisj  35381  mblfinlem2  35815  volsupnfl  35822  12gcd5e1  40011  ifpdfor  41072  ifpim1  41076  ifpnot  41077  ifpid2  41078  ifpim2  41079  ifpim1g  41108  ifpbi1b  41110  icccncfext  43428  fourierdlem103  43750  fourierdlem104  43751  etransclem24  43799  etransclem35  43810  abnotataxb  44411  dandysum2p2e4  44493  paireqne  44963  sbgoldbo  45239  zlmodzxzldeplem  45839  line2x  46100  aacllem  46505