Theorem olci 867

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

Syntax hints:  ¬ wn 3   ∨ wo 848

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 849

This theorem is referenced by:  falortru  1581  opthhausdorff  5473  sucidg  6408  f1ounsn  7228  kmlem2  10074  sornom  10199  leid  11241  pnf0xnn0  12493  xrleid  13077  xmul01  13194  bcn1  14248  odd2np1lem  16279  lcm0val  16533  lcmfunsnlem2lem1  16577  lcmfunsnlem2  16579  coprmprod  16600  coprmproddvdslem  16601  prmrec  16862  smndex2dnrinv  18852  m2detleib  22587  zclmncvs  25116  itg0  25749  itgz  25750  coemullem  26223  ftalem5  27055  chp1  27145  prmorcht  27156  pclogsum  27194  logexprlim  27204  bpos1  27262  addsqnreup  27422  pntpbnd1  27565  axlowdimlem16  29042  usgrexmpldifpr  29343  cusgrsizeindb1  29536  pthdlem2  29853  ex-or  30508  ply1coedeg  33681  plymulx0  34724  signstfvn  34746  bj-0eltag  37220  bj-inftyexpidisj  37459  mblfinlem2  37903  volsupnfl  37910  12gcd5e1  42367  ifpdfor  43815  ifpim1  43819  ifpnot  43820  ifpid2  43821  ifpim2  43822  ifpim1g  43851  ifpbi1b  43853  icccncfext  46239  fourierdlem103  46561  fourierdlem104  46562  etransclem24  46610  etransclem35  46621  abnotataxb  47270  dandysum2p2e4  47352  paireqne  47865  sbgoldbo  48141  usgrexmpl1lem  48375  usgrexmpl1tri  48379  usgrexmpl2lem  48380  usgrexmpl2nb0  48385  usgrexmpl2nb2  48387  usgrexmpl2nb3  48388  usgrexmpl2nb4  48389  usgrexmpl2nb5  48390  gpgedg2iv  48421  gpg5nbgrvtx03starlem2  48423  gpg5nbgrvtx13starlem2  48426  gpgprismgr4cycllem2  48450  gpgprismgr4cycllem7  48455  gpg5edgnedg  48484  zlmodzxzldeplem  48852  line2x  49108  aacllem  50154