Theorem olci 867

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

Syntax hints:  ¬ wn 3   ∨ wo 848

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 849

This theorem is referenced by:  falortru  1581  opthhausdorff  5465  sucidg  6400  f1ounsn  7220  kmlem2  10065  sornom  10190  leid  11233  pnf0xnn0  12508  xrleid  13093  xmul01  13210  bcn1  14266  odd2np1lem  16300  lcm0val  16554  lcmfunsnlem2lem1  16598  lcmfunsnlem2  16600  coprmprod  16621  coprmproddvdslem  16622  prmrec  16884  smndex2dnrinv  18877  m2detleib  22606  zclmncvs  25125  itg0  25757  itgz  25758  coemullem  26225  ftalem5  27054  chp1  27144  prmorcht  27155  pclogsum  27192  logexprlim  27202  bpos1  27260  addsqnreup  27420  pntpbnd1  27563  axlowdimlem16  29040  usgrexmpldifpr  29341  cusgrsizeindb1  29534  pthdlem2  29851  ex-or  30506  ply1coedeg  33664  plymulx0  34707  signstfvn  34729  bj-0eltag  37301  bj-inftyexpidisj  37540  mblfinlem2  37993  volsupnfl  38000  12gcd5e1  42456  ifpdfor  43910  ifpim1  43914  ifpnot  43915  ifpid2  43916  ifpim2  43917  ifpim1g  43946  ifpbi1b  43948  icccncfext  46333  fourierdlem103  46655  fourierdlem104  46656  etransclem24  46704  etransclem35  46715  abnotataxb  47376  dandysum2p2e4  47458  paireqne  47983  sbgoldbo  48275  usgrexmpl1lem  48509  usgrexmpl1tri  48513  usgrexmpl2lem  48514  usgrexmpl2nb0  48519  usgrexmpl2nb2  48521  usgrexmpl2nb3  48522  usgrexmpl2nb4  48523  usgrexmpl2nb5  48524  gpgedg2iv  48555  gpg5nbgrvtx03starlem2  48557  gpg5nbgrvtx13starlem2  48560  gpgprismgr4cycllem2  48584  gpgprismgr4cycllem7  48589  gpg5edgnedg  48618  zlmodzxzldeplem  48986  line2x  49242  aacllem  50288