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  5479  sucidg  6417  f1ounsn  7249  kmlem2  10111  sornom  10236  leid  11276  pnf0xnn0  12528  xrleid  13117  xmul01  13233  bcn1  14284  odd2np1lem  16316  lcm0val  16570  lcmfunsnlem2lem1  16614  lcmfunsnlem2  16616  coprmprod  16637  coprmproddvdslem  16638  prmrec  16899  smndex2dnrinv  18848  m2detleib  22524  zclmncvs  25054  itg0  25687  itgz  25688  coemullem  26161  ftalem5  26993  chp1  27083  prmorcht  27094  pclogsum  27132  logexprlim  27142  bpos1  27200  addsqnreup  27360  pntpbnd1  27503  axlowdimlem16  28890  usgrexmpldifpr  29191  cusgrsizeindb1  29384  pthdlem2  29704  ex-or  30356  plymulx0  34544  signstfvn  34566  bj-0eltag  36961  bj-inftyexpidisj  37193  mblfinlem2  37647  volsupnfl  37654  12gcd5e1  41986  ifpdfor  43447  ifpim1  43451  ifpnot  43452  ifpid2  43453  ifpim2  43454  ifpim1g  43483  ifpbi1b  43485  icccncfext  45878  fourierdlem103  46200  fourierdlem104  46201  etransclem24  46249  etransclem35  46260  abnotataxb  46907  dandysum2p2e4  46989  paireqne  47502  sbgoldbo  47778  usgrexmpl1lem  48002  usgrexmpl1tri  48006  usgrexmpl2lem  48007  usgrexmpl2nb0  48012  usgrexmpl2nb2  48014  usgrexmpl2nb3  48015  usgrexmpl2nb4  48016  usgrexmpl2nb5  48017  gpgedg2iv  48048  gpg5nbgrvtx03starlem2  48050  gpg5nbgrvtx13starlem2  48053  gpgprismgr4cycllem2  48076  gpgprismgr4cycllem7  48081  zlmodzxzldeplem  48477  line2x  48733  aacllem  49767