Theorem olci 866

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

Syntax hints:  ¬ wn 3   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  falortru  1575  opthhausdorff  5526  sucidg  6466  f1ounsn  7291  kmlem2  10189  sornom  10314  leid  11354  pnf0xnn0  12603  xrleid  13189  xmul01  13305  bcn1  14348  odd2np1lem  16373  lcm0val  16627  lcmfunsnlem2lem1  16671  lcmfunsnlem2  16673  coprmprod  16694  coprmproddvdslem  16695  prmrec  16955  smndex2dnrinv  18940  sratsetOLD  21206  sradsOLD  21209  m2detleib  22652  zclmncvs  25195  itg0  25829  itgz  25830  coemullem  26303  ftalem5  27134  chp1  27224  prmorcht  27235  pclogsum  27273  logexprlim  27283  bpos1  27341  addsqnreup  27501  pntpbnd1  27644  nohalf  28421  axlowdimlem16  28986  usgrexmpldifpr  29289  cusgrsizeindb1  29482  pthdlem2  29800  ex-or  30449  plymulx0  34540  signstfvn  34562  bj-0eltag  36960  bj-inftyexpidisj  37192  mblfinlem2  37644  volsupnfl  37651  12gcd5e1  41984  ifpdfor  43454  ifpim1  43458  ifpnot  43459  ifpid2  43460  ifpim2  43461  ifpim1g  43490  ifpbi1b  43492  icccncfext  45842  fourierdlem103  46164  fourierdlem104  46165  etransclem24  46213  etransclem35  46224  abnotataxb  46865  dandysum2p2e4  46947  paireqne  47435  sbgoldbo  47711  usgrexmpl1lem  47915  usgrexmpl1tri  47919  usgrexmpl2lem  47920  usgrexmpl2nb0  47925  usgrexmpl2nb2  47927  usgrexmpl2nb3  47928  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx13starlem2  47962  zlmodzxzldeplem  48343  line2x  48603  aacllem  49031