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  1579  opthhausdorff  5464  sucidg  6394  f1ounsn  7213  kmlem2  10065  sornom  10190  leid  11230  pnf0xnn0  12482  xrleid  13071  xmul01  13187  bcn1  14238  odd2np1lem  16269  lcm0val  16523  lcmfunsnlem2lem1  16567  lcmfunsnlem2  16569  coprmprod  16590  coprmproddvdslem  16591  prmrec  16852  smndex2dnrinv  18807  m2detleib  22534  zclmncvs  25064  itg0  25697  itgz  25698  coemullem  26171  ftalem5  27003  chp1  27093  prmorcht  27104  pclogsum  27142  logexprlim  27152  bpos1  27210  addsqnreup  27370  pntpbnd1  27513  axlowdimlem16  28920  usgrexmpldifpr  29221  cusgrsizeindb1  29414  pthdlem2  29731  ex-or  30383  plymulx0  34514  signstfvn  34536  bj-0eltag  36951  bj-inftyexpidisj  37183  mblfinlem2  37637  volsupnfl  37644  12gcd5e1  41976  ifpdfor  43438  ifpim1  43442  ifpnot  43443  ifpid2  43444  ifpim2  43445  ifpim1g  43474  ifpbi1b  43476  icccncfext  45869  fourierdlem103  46191  fourierdlem104  46192  etransclem24  46240  etransclem35  46251  abnotataxb  46901  dandysum2p2e4  46983  paireqne  47496  sbgoldbo  47772  usgrexmpl1lem  48006  usgrexmpl1tri  48010  usgrexmpl2lem  48011  usgrexmpl2nb0  48016  usgrexmpl2nb2  48018  usgrexmpl2nb3  48019  usgrexmpl2nb4  48020  usgrexmpl2nb5  48021  gpgedg2iv  48052  gpg5nbgrvtx03starlem2  48054  gpg5nbgrvtx13starlem2  48057  gpgprismgr4cycllem2  48081  gpgprismgr4cycllem7  48086  gpg5edgnedg  48115  zlmodzxzldeplem  48484  line2x  48740  aacllem  49787