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  5480  sucidg  6418  f1ounsn  7250  kmlem2  10112  sornom  10237  leid  11277  pnf0xnn0  12529  xrleid  13118  xmul01  13234  bcn1  14285  odd2np1lem  16317  lcm0val  16571  lcmfunsnlem2lem1  16615  lcmfunsnlem2  16617  coprmprod  16638  coprmproddvdslem  16639  prmrec  16900  smndex2dnrinv  18849  m2detleib  22525  zclmncvs  25055  itg0  25688  itgz  25689  coemullem  26162  ftalem5  26994  chp1  27084  prmorcht  27095  pclogsum  27133  logexprlim  27143  bpos1  27201  addsqnreup  27361  pntpbnd1  27504  axlowdimlem16  28891  usgrexmpldifpr  29192  cusgrsizeindb1  29385  pthdlem2  29705  ex-or  30357  plymulx0  34545  signstfvn  34567  bj-0eltag  36973  bj-inftyexpidisj  37205  mblfinlem2  37659  volsupnfl  37666  12gcd5e1  41998  ifpdfor  43461  ifpim1  43465  ifpnot  43466  ifpid2  43467  ifpim2  43468  ifpim1g  43497  ifpbi1b  43499  icccncfext  45892  fourierdlem103  46214  fourierdlem104  46215  etransclem24  46263  etransclem35  46274  abnotataxb  46921  dandysum2p2e4  47003  paireqne  47516  sbgoldbo  47792  usgrexmpl1lem  48016  usgrexmpl1tri  48020  usgrexmpl2lem  48021  usgrexmpl2nb0  48026  usgrexmpl2nb2  48028  usgrexmpl2nb3  48029  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  gpgedg2iv  48062  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx13starlem2  48067  gpgprismgr4cycllem2  48090  gpgprismgr4cycllem7  48095  zlmodzxzldeplem  48491  line2x  48747  aacllem  49794