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  1580  opthhausdorff  5465  sucidg  6400  f1ounsn  7218  kmlem2  10062  sornom  10187  leid  11229  pnf0xnn0  12481  xrleid  13065  xmul01  13182  bcn1  14236  odd2np1lem  16267  lcm0val  16521  lcmfunsnlem2lem1  16565  lcmfunsnlem2  16567  coprmprod  16588  coprmproddvdslem  16589  prmrec  16850  smndex2dnrinv  18840  m2detleib  22575  zclmncvs  25104  itg0  25737  itgz  25738  coemullem  26211  ftalem5  27043  chp1  27133  prmorcht  27144  pclogsum  27182  logexprlim  27192  bpos1  27250  addsqnreup  27410  pntpbnd1  27553  axlowdimlem16  29030  usgrexmpldifpr  29331  cusgrsizeindb1  29524  pthdlem2  29841  ex-or  30496  ply1coedeg  33670  plymulx0  34704  signstfvn  34726  bj-0eltag  37179  bj-inftyexpidisj  37411  mblfinlem2  37855  volsupnfl  37862  12gcd5e1  42253  ifpdfor  43702  ifpim1  43706  ifpnot  43707  ifpid2  43708  ifpim2  43709  ifpim1g  43738  ifpbi1b  43740  icccncfext  46127  fourierdlem103  46449  fourierdlem104  46450  etransclem24  46498  etransclem35  46509  abnotataxb  47158  dandysum2p2e4  47240  paireqne  47753  sbgoldbo  48029  usgrexmpl1lem  48263  usgrexmpl1tri  48267  usgrexmpl2lem  48268  usgrexmpl2nb0  48273  usgrexmpl2nb2  48275  usgrexmpl2nb3  48276  usgrexmpl2nb4  48277  usgrexmpl2nb5  48278  gpgedg2iv  48309  gpg5nbgrvtx03starlem2  48311  gpg5nbgrvtx13starlem2  48314  gpgprismgr4cycllem2  48338  gpgprismgr4cycllem7  48343  gpg5edgnedg  48372  zlmodzxzldeplem  48740  line2x  48996  aacllem  50042