Theorem olci 879

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

Syntax hints:  ¬ wn 3   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  falortru  1602  opthhausdorff  5491  sucidg  6433  f1ounsn  7260  kmlem2  10123  sornom  10249  leid  11294  pnf0xnn0  12575  xrleid  13167  xmul01  13284  bcn1  14340  odd2np1lem  16388  lcm0val  16642  lcmfunsnlem2lem1  16686  lcmfunsnlem2  16688  coprmprod  16709  coprmproddvdslem  16710  prmrec  16972  smndex2dnrinv  18967  m2detleib  22749  zclmncvs  25268  itg0  25900  itgz  25901  coemullem  26368  plyn0mulidp  26403  ftalem5  27199  chp1  27289  prmorcht  27300  pclogsum  27337  logexprlim  27347  bpos1  27405  addsqnreup  27565  pntpbnd1  27708  axlowdimlem16  29216  usgrexmpldifpr  29517  cusgrsizeindb1  29709  pthdlem2  30026  ex-or  30681  ply1coedeg  33796  signstfvn  34873  bj-0eltag  37475  bj-inftyexpidisj  37714  mblfinlem2  38169  volsupnfl  38176  12gcd5e1  42632  ifpdfor  44053  ifpim1  44057  ifpnot  44058  ifpid2  44059  ifpim2  44060  ifpim1g  44089  ifpbi1b  44091  icccncfext  46459  fourierdlem103  46781  fourierdlem104  46782  etransclem24  46830  etransclem35  46841  abnotataxb  47508  dandysum2p2e4  47590  paireqne  48115  sbgoldbo  48407  usgrexmpl1lem  48641  usgrexmpl1tri  48645  usgrexmpl2lem  48646  usgrexmpl2nb0  48651  usgrexmpl2nb2  48653  usgrexmpl2nb3  48654  usgrexmpl2nb4  48655  usgrexmpl2nb5  48656  gpgedg2iv  48687  gpg5nbgrvtx03starlem2  48689  gpg5nbgrvtx13starlem2  48692  gpgprismgr4cycllem2  48716  gpgprismgr4cycllem7  48721  gpg5edgnedg  48750  zlmodzxzldeplem  49129  line2x  49385  aacllem  50430