Theorem olci 867

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

Syntax hints:  ¬ wn 3   ∨ wo 848

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 849

This theorem is referenced by:  falortru  1579  opthhausdorff  5522  sucidg  6465  f1ounsn  7292  kmlem2  10192  sornom  10317  leid  11357  pnf0xnn0  12606  xrleid  13193  xmul01  13309  bcn1  14352  odd2np1lem  16377  lcm0val  16631  lcmfunsnlem2lem1  16675  lcmfunsnlem2  16677  coprmprod  16698  coprmproddvdslem  16699  prmrec  16960  smndex2dnrinv  18928  sratsetOLD  21189  sradsOLD  21192  m2detleib  22637  zclmncvs  25182  itg0  25815  itgz  25816  coemullem  26289  ftalem5  27120  chp1  27210  prmorcht  27221  pclogsum  27259  logexprlim  27269  bpos1  27327  addsqnreup  27487  pntpbnd1  27630  nohalf  28407  axlowdimlem16  28972  usgrexmpldifpr  29275  cusgrsizeindb1  29468  pthdlem2  29788  ex-or  30440  plymulx0  34562  signstfvn  34584  bj-0eltag  36979  bj-inftyexpidisj  37211  mblfinlem2  37665  volsupnfl  37672  12gcd5e1  42004  ifpdfor  43478  ifpim1  43482  ifpnot  43483  ifpid2  43484  ifpim2  43485  ifpim1g  43514  ifpbi1b  43516  icccncfext  45902  fourierdlem103  46224  fourierdlem104  46225  etransclem24  46273  etransclem35  46284  abnotataxb  46928  dandysum2p2e4  47010  paireqne  47498  sbgoldbo  47774  usgrexmpl1lem  47980  usgrexmpl1tri  47984  usgrexmpl2lem  47985  usgrexmpl2nb0  47990  usgrexmpl2nb2  47992  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx13starlem2  48028  zlmodzxzldeplem  48415  line2x  48675  aacllem  49320