Theorem olci 865

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

Syntax hints:  ¬ wn 3   ∨ wo 846

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 847

This theorem is referenced by:  falortru  1576  opthhausdorff  5536  sucidg  6476  kmlem2  10221  sornom  10346  leid  11386  pnf0xnn0  12632  xrleid  13213  xmul01  13329  bcn1  14362  odd2np1lem  16388  lcm0val  16641  lcmfunsnlem2lem1  16685  lcmfunsnlem2  16687  coprmprod  16708  coprmproddvdslem  16709  prmrec  16969  smndex2dnrinv  18950  sratsetOLD  21212  sradsOLD  21215  m2detleib  22658  zclmncvs  25201  itg0  25835  itgz  25836  coemullem  26309  ftalem5  27138  chp1  27228  prmorcht  27239  pclogsum  27277  logexprlim  27287  bpos1  27345  addsqnreup  27505  pntpbnd1  27648  nohalf  28425  axlowdimlem16  28990  usgrexmpldifpr  29293  cusgrsizeindb1  29486  pthdlem2  29804  ex-or  30453  plymulx0  34524  signstfvn  34546  bj-0eltag  36944  bj-inftyexpidisj  37176  mblfinlem2  37618  volsupnfl  37625  12gcd5e1  41960  ifpdfor  43427  ifpim1  43431  ifpnot  43432  ifpid2  43433  ifpim2  43434  ifpim1g  43463  ifpbi1b  43465  icccncfext  45808  fourierdlem103  46130  fourierdlem104  46131  etransclem24  46179  etransclem35  46190  abnotataxb  46831  dandysum2p2e4  46913  paireqne  47385  sbgoldbo  47661  usgrexmpl1lem  47836  usgrexmpl1tri  47840  usgrexmpl2lem  47841  usgrexmpl2nb0  47846  usgrexmpl2nb2  47848  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  zlmodzxzldeplem  48227  line2x  48488  aacllem  48895