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  1609  opthhausdorff  5502  sucidg  6446  f1ounsn  7272  kmlem2  10136  sornom  10262  leid  11307  pnf0xnn0  12585  xrleid  13177  xmul01  13294  bcn1  14351  odd2np1lem  16399  lcm0val  16653  lcmfunsnlem2lem1  16697  lcmfunsnlem2  16699  coprmprod  16720  coprmproddvdslem  16721  prmrec  16983  smndex2dnrinv  18978  m2detleib  22769  zclmncvs  25288  itg0  25920  itgz  25921  coemullem  26388  plyn0mulidp  26423  ftalem5  27222  chp1  27312  prmorcht  27323  pclogsum  27360  logexprlim  27370  bpos1  27428  addsqnreup  27588  pntpbnd1  27731  axlowdimlem16  29288  usgrexmpldifpr  29589  cusgrsizeindb1  29781  pthdlem2  30098  ex-or  30753  ply1coedeg  33860  signstfvn  34937  bj-0eltag  37595  bj-inftyexpidisj  37835  mblfinlem2  38290  volsupnfl  38297  12gcd5e1  42751  ifpdfor  44174  ifpim1  44178  ifpnot  44179  ifpid2  44180  ifpim2  44181  ifpim1g  44210  ifpbi1b  44212  icccncfext  46584  fourierdlem103  46906  fourierdlem104  46907  etransclem24  46955  etransclem35  46966  abnotataxb  47636  dandysum2p2e4  47718  paireqne  48243  sbgoldbo  48535  usgrexmpl1lem  48769  usgrexmpl1tri  48773  usgrexmpl2lem  48774  usgrexmpl2nb0  48779  usgrexmpl2nb2  48781  usgrexmpl2nb3  48782  usgrexmpl2nb4  48783  usgrexmpl2nb5  48784  gpgedg2iv  48815  gpg5nbgrvtx03starlem2  48817  gpg5nbgrvtx13starlem2  48820  gpgprismgr4cycllem2  48844  gpgprismgr4cycllem7  48849  gpg5edgnedg  48878  zlmodzxzldeplem  49261  line2x  49517  aacllem  50584