Theorem olci 872

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

Syntax hints:  ¬ wn 3   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  falortru  1586  opthhausdorff  5465  sucidg  6400  f1ounsn  7223  kmlem2  10072  sornom  10197  leid  11240  pnf0xnn0  12515  xrleid  13100  xmul01  13217  bcn1  14273  odd2np1lem  16307  lcm0val  16561  lcmfunsnlem2lem1  16605  lcmfunsnlem2  16607  coprmprod  16628  coprmproddvdslem  16629  prmrec  16891  smndex2dnrinv  18884  m2detleib  22621  zclmncvs  25140  itg0  25772  itgz  25773  coemullem  26240  ftalem5  27065  chp1  27155  prmorcht  27166  pclogsum  27203  logexprlim  27213  bpos1  27271  addsqnreup  27431  pntpbnd1  27574  axlowdimlem16  29051  usgrexmpldifpr  29352  cusgrsizeindb1  29544  pthdlem2  29861  ex-or  30516  ply1coedeg  33679  plymulx0  34738  signstfvn  34760  bj-0eltag  37338  bj-inftyexpidisj  37577  mblfinlem2  38032  volsupnfl  38039  12gcd5e1  42495  ifpdfor  43916  ifpim1  43920  ifpnot  43921  ifpid2  43922  ifpim2  43923  ifpim1g  43952  ifpbi1b  43954  icccncfext  46337  fourierdlem103  46659  fourierdlem104  46660  etransclem24  46708  etransclem35  46719  abnotataxb  47386  dandysum2p2e4  47468  paireqne  47993  sbgoldbo  48285  usgrexmpl1lem  48519  usgrexmpl1tri  48523  usgrexmpl2lem  48524  usgrexmpl2nb0  48529  usgrexmpl2nb2  48531  usgrexmpl2nb3  48532  usgrexmpl2nb4  48533  usgrexmpl2nb5  48534  gpgedg2iv  48565  gpg5nbgrvtx03starlem2  48567  gpg5nbgrvtx13starlem2  48570  gpgprismgr4cycllem2  48594  gpgprismgr4cycllem7  48599  gpg5edgnedg  48628  zlmodzxzldeplem  48996  line2x  49252  aacllem  50298