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  1579  opthhausdorff  5477  sucidg  6415  f1ounsn  7247  kmlem2  10105  sornom  10230  leid  11270  pnf0xnn0  12522  xrleid  13111  xmul01  13227  bcn1  14278  odd2np1lem  16310  lcm0val  16564  lcmfunsnlem2lem1  16608  lcmfunsnlem2  16610  coprmprod  16631  coprmproddvdslem  16632  prmrec  16893  smndex2dnrinv  18842  m2detleib  22518  zclmncvs  25048  itg0  25681  itgz  25682  coemullem  26155  ftalem5  26987  chp1  27077  prmorcht  27088  pclogsum  27126  logexprlim  27136  bpos1  27194  addsqnreup  27354  pntpbnd1  27497  axlowdimlem16  28884  usgrexmpldifpr  29185  cusgrsizeindb1  29378  pthdlem2  29698  ex-or  30350  plymulx0  34538  signstfvn  34560  bj-0eltag  36966  bj-inftyexpidisj  37198  mblfinlem2  37652  volsupnfl  37659  12gcd5e1  41991  ifpdfor  43454  ifpim1  43458  ifpnot  43459  ifpid2  43460  ifpim2  43461  ifpim1g  43490  ifpbi1b  43492  icccncfext  45885  fourierdlem103  46207  fourierdlem104  46208  etransclem24  46256  etransclem35  46267  abnotataxb  46917  dandysum2p2e4  46999  paireqne  47512  sbgoldbo  47788  usgrexmpl1lem  48012  usgrexmpl1tri  48016  usgrexmpl2lem  48017  usgrexmpl2nb0  48022  usgrexmpl2nb2  48024  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  gpgedg2iv  48058  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx13starlem2  48063  gpgprismgr4cycllem2  48086  gpgprismgr4cycllem7  48091  zlmodzxzldeplem  48487  line2x  48743  aacllem  49790