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  5492  sucidg  6434  f1ounsn  7264  kmlem2  10164  sornom  10289  leid  11329  pnf0xnn0  12579  xrleid  13165  xmul01  13281  bcn1  14329  odd2np1lem  16357  lcm0val  16611  lcmfunsnlem2lem1  16655  lcmfunsnlem2  16657  coprmprod  16678  coprmproddvdslem  16679  prmrec  16940  smndex2dnrinv  18891  m2detleib  22567  zclmncvs  25098  itg0  25731  itgz  25732  coemullem  26205  ftalem5  27037  chp1  27127  prmorcht  27138  pclogsum  27176  logexprlim  27186  bpos1  27244  addsqnreup  27404  pntpbnd1  27547  nohalf  28324  axlowdimlem16  28882  usgrexmpldifpr  29183  cusgrsizeindb1  29376  pthdlem2  29696  ex-or  30348  plymulx0  34525  signstfvn  34547  bj-0eltag  36942  bj-inftyexpidisj  37174  mblfinlem2  37628  volsupnfl  37635  12gcd5e1  41962  ifpdfor  43436  ifpim1  43440  ifpnot  43441  ifpid2  43442  ifpim2  43443  ifpim1g  43472  ifpbi1b  43474  icccncfext  45864  fourierdlem103  46186  fourierdlem104  46187  etransclem24  46235  etransclem35  46246  abnotataxb  46893  dandysum2p2e4  46975  paireqne  47473  sbgoldbo  47749  usgrexmpl1lem  47973  usgrexmpl1tri  47977  usgrexmpl2lem  47978  usgrexmpl2nb0  47983  usgrexmpl2nb2  47985  usgrexmpl2nb3  47986  usgrexmpl2nb4  47987  usgrexmpl2nb5  47988  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx13starlem2  48022  gpgprismgr4cycllem2  48043  gpgprismgr4cycllem7  48048  zlmodzxzldeplem  48422  line2x  48682  aacllem  49613