Theorem olci 862

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

Syntax hints:  ¬ wn 3   ∨ wo 843

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 206  df-or 844

This theorem is referenced by:  falortru  1578  opthhausdorff  5425  sucidg  6329  kmlem2  9838  sornom  9964  leid  11001  pnf0xnn0  12242  xrleid  12814  xmul01  12930  bcn1  13955  odd2np1lem  15977  lcm0val  16227  lcmfunsnlem2lem1  16271  lcmfunsnlem2  16273  coprmprod  16294  coprmproddvdslem  16295  prmrec  16551  smndex2dnrinv  18469  sratsetOLD  20366  sradsOLD  20369  m2detleib  21688  zclmncvs  24217  itg0  24849  itgz  24850  coemullem  25316  ftalem5  26131  chp1  26221  prmorcht  26232  pclogsum  26268  logexprlim  26278  bpos1  26336  addsqnreup  26496  pntpbnd1  26639  axlowdimlem16  27228  usgrexmpldifpr  27528  cusgrsizeindb1  27720  pthdlem2  28037  ex-or  28686  plymulx0  32426  signstfvn  32448  bj-0eltag  35095  bj-inftyexpidisj  35308  mblfinlem2  35742  volsupnfl  35749  12gcd5e1  39939  ifpdfor  40970  ifpim1  40974  ifpnot  40975  ifpid2  40976  ifpim2  40977  ifpim1g  41006  ifpbi1b  41008  icccncfext  43318  fourierdlem103  43640  fourierdlem104  43641  etransclem24  43689  etransclem35  43700  abnotataxb  44298  dandysum2p2e4  44380  paireqne  44851  sbgoldbo  45127  zlmodzxzldeplem  45727  line2x  45988  aacllem  46391