Theorem olci 880

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

This proof depends on syntax axioms:  ¬ wn 3   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  falortru  1609  opthhausdorff  5505  sucidg  6451  f1ounsn  7281  kmlem2  10154  sornom  10279  leid  11324  pnf0xnn0  12602  xrleid  13194  xmul01  13311  bcn1  14369  odd2np1lem  16423  lcm0val  16677  lcmfunsnlem2lem1  16721  lcmfunsnlem2  16723  coprmprod  16744  coprmproddvdslem  16745  prmrec  17007  smndex2dnrinv  19008  m2detleib  22825  zclmncvs  25344  itg0  25976  itgz  25977  coemullem  26444  plyn0mulidp  26479  ftalem5  27278  chp1  27368  prmorcht  27379  pclogsum  27416  logexprlim  27426  bpos1  27484  addsqnreup  27644  pntpbnd1  27787  axlowdimlem16  29344  usgrexmpldifpr  29645  cusgrsizeindb1  29837  pthdlem2  30154  ex-or  30809  ply1coedeg  33910  signstfvn  34988  bj-0eltag  37655  bj-inftyexpidisj  37895  mblfinlem2  38350  volsupnfl  38357  12gcd5e1  42811  ifpdfor  44232  ifpim1  44236  ifpnot  44237  ifpid2  44238  ifpim2  44239  ifpim1g  44268  ifpbi1b  44270  icccncfext  46642  fourierdlem103  46964  fourierdlem104  46965  etransclem24  47013  etransclem35  47024  abnotataxb  47694  dandysum2p2e4  47776  paireqne  48301  sbgoldbo  48593  usgrexmpl1lem  48827  usgrexmpl1tri  48831  usgrexmpl2lem  48832  usgrexmpl2nb0  48837  usgrexmpl2nb2  48839  usgrexmpl2nb3  48840  usgrexmpl2nb4  48841  usgrexmpl2nb5  48842  gpgedg2iv  48873  gpg5nbgrvtx03starlem2  48875  gpg5nbgrvtx13starlem2  48878  gpgprismgr4cycllem2  48902  gpgprismgr4cycllem7  48907  gpg5edgnedg  48936  zlmodzxzldeplem  49319  line2x  49575  aacllem  50662