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  1580  opthhausdorff  5460  sucidg  6394  f1ounsn  7212  kmlem2  10050  sornom  10175  leid  11216  pnf0xnn0  12468  xrleid  13052  xmul01  13168  bcn1  14222  odd2np1lem  16253  lcm0val  16507  lcmfunsnlem2lem1  16551  lcmfunsnlem2  16553  coprmprod  16574  coprmproddvdslem  16575  prmrec  16836  smndex2dnrinv  18825  m2detleib  22547  zclmncvs  25076  itg0  25709  itgz  25710  coemullem  26183  ftalem5  27015  chp1  27105  prmorcht  27116  pclogsum  27154  logexprlim  27164  bpos1  27222  addsqnreup  27382  pntpbnd1  27525  axlowdimlem16  28937  usgrexmpldifpr  29238  cusgrsizeindb1  29431  pthdlem2  29748  ex-or  30403  plymulx0  34581  signstfvn  34603  bj-0eltag  37043  bj-inftyexpidisj  37275  mblfinlem2  37718  volsupnfl  37725  12gcd5e1  42116  ifpdfor  43582  ifpim1  43586  ifpnot  43587  ifpid2  43588  ifpim2  43589  ifpim1g  43618  ifpbi1b  43620  icccncfext  46009  fourierdlem103  46331  fourierdlem104  46332  etransclem24  46380  etransclem35  46391  abnotataxb  47040  dandysum2p2e4  47122  paireqne  47635  sbgoldbo  47911  usgrexmpl1lem  48145  usgrexmpl1tri  48149  usgrexmpl2lem  48150  usgrexmpl2nb0  48155  usgrexmpl2nb2  48157  usgrexmpl2nb3  48158  usgrexmpl2nb4  48159  usgrexmpl2nb5  48160  gpgedg2iv  48191  gpg5nbgrvtx03starlem2  48193  gpg5nbgrvtx13starlem2  48196  gpgprismgr4cycllem2  48220  gpgprismgr4cycllem7  48225  gpg5edgnedg  48254  zlmodzxzldeplem  48623  line2x  48879  aacllem  49926