Theorem olci 877

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

Syntax hints:  ¬ wn 3   ∨ wo 858

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 209  df-or 859

This theorem is referenced by:  falortru  1598  opthhausdorff  5485  sucidg  6425  f1ounsn  7252  kmlem2  10105  sornom  10231  leid  11276  pnf0xnn0  12558  xrleid  13150  xmul01  13267  bcn1  14323  odd2np1lem  16357  lcm0val  16611  lcmfunsnlem2lem1  16655  lcmfunsnlem2  16657  coprmprod  16678  coprmproddvdslem  16679  prmrec  16941  smndex2dnrinv  18935  m2detleib  22671  zclmncvs  25190  itg0  25822  itgz  25823  coemullem  26290  ftalem5  27118  chp1  27208  prmorcht  27219  pclogsum  27256  logexprlim  27266  bpos1  27324  addsqnreup  27484  pntpbnd1  27627  axlowdimlem16  29104  usgrexmpldifpr  29405  cusgrsizeindb1  29597  pthdlem2  29914  ex-or  30569  ply1coedeg  33746  plymulx0  34805  signstfvn  34827  bj-0eltag  37427  bj-inftyexpidisj  37666  mblfinlem2  38121  volsupnfl  38128  12gcd5e1  42584  ifpdfor  44005  ifpim1  44009  ifpnot  44010  ifpid2  44011  ifpim2  44012  ifpim1g  44041  ifpbi1b  44043  icccncfext  46425  fourierdlem103  46747  fourierdlem104  46748  etransclem24  46796  etransclem35  46807  abnotataxb  47474  dandysum2p2e4  47556  paireqne  48081  sbgoldbo  48373  usgrexmpl1lem  48607  usgrexmpl1tri  48611  usgrexmpl2lem  48612  usgrexmpl2nb0  48617  usgrexmpl2nb2  48619  usgrexmpl2nb3  48620  usgrexmpl2nb4  48621  usgrexmpl2nb5  48622  gpgedg2iv  48653  gpg5nbgrvtx03starlem2  48655  gpg5nbgrvtx13starlem2  48658  gpgprismgr4cycllem2  48682  gpgprismgr4cycllem7  48687  gpg5edgnedg  48716  zlmodzxzldeplem  49084  line2x  49340  aacllem  50386