Theorem olci 864

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

Syntax hints:  ¬ wn 3   ∨ wo 845

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 846

This theorem is referenced by:  falortru  1572  opthhausdorff  5519  sucidg  6452  kmlem2  10176  sornom  10302  leid  11342  pnf0xnn0  12584  xrleid  13165  xmul01  13281  bcn1  14308  odd2np1lem  16320  lcm0val  16568  lcmfunsnlem2lem1  16612  lcmfunsnlem2  16614  coprmprod  16635  coprmproddvdslem  16636  prmrec  16894  smndex2dnrinv  18875  sratsetOLD  21087  sradsOLD  21090  m2detleib  22577  zclmncvs  25120  itg0  25753  itgz  25754  coemullem  26229  ftalem5  27054  chp1  27144  prmorcht  27155  pclogsum  27193  logexprlim  27203  bpos1  27261  addsqnreup  27421  pntpbnd1  27564  axlowdimlem16  28840  usgrexmpldifpr  29143  cusgrsizeindb1  29336  pthdlem2  29654  ex-or  30303  plymulx0  34310  signstfvn  34332  bj-0eltag  36588  bj-inftyexpidisj  36820  mblfinlem2  37262  volsupnfl  37269  12gcd5e1  41606  ifpdfor  43037  ifpim1  43041  ifpnot  43042  ifpid2  43043  ifpim2  43044  ifpim1g  43073  ifpbi1b  43075  icccncfext  45413  fourierdlem103  45735  fourierdlem104  45736  etransclem24  45784  etransclem35  45795  abnotataxb  46436  dandysum2p2e4  46518  paireqne  46988  sbgoldbo  47264  zlmodzxzldeplem  47752  line2x  48013  aacllem  48420