Theorem olci 880

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

This proof depends on syntax axioms:  ¬ wn 3   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  falortru  1608  opthhausdorff  5489  sucidg  6446  f1ounsn  7280  kmlem2  10233  sornom  10358  leid  11409  pnf0xnn0  12689  xrleid  13283  xmul01  13400  bcn1  14460  odd2np1lem  16515  lcm0val  16774  lcmfunsnlem2lem1  16818  lcmfunsnlem2  16820  coprmprod  16841  coprmproddvdslem  16842  prmrec  17105  smndex2dnrinv  19119  degenmgm  19142  degenmgm2  19145  m2detleib  22951  zclmncvs  25474  itg0  26105  itgz  26106  coemullem  26574  plyn0mulidp  26607  ftalem5  27409  chp1  27499  prmorcht  27510  pclogsum  27547  logexprlim  27557  bpos1  27615  addsqnreup  27775  pntpbnd1  27918  axlowdimlem16  29540  usgrexmpldifpr  29844  cusgrsizeindb1  30036  pthdlem2  30359  ex-or  31027  ply1coedeg  34167  signstfvn  35244  bj-0eltag  37983  bj-inftyexpidisj  38224  mblfinlem2  38669  volsupnfl  38676  12gcd5e1  43146  ifpdfor  44559  ifpim1  44563  ifpnot  44564  ifpid2  44565  ifpim2  44566  ifpim1g  44595  ifpbi1b  44597  icccncfext  46990  fourierdlem103  47312  fourierdlem104  47313  etransclem24  47361  etransclem35  47372  abnotataxb  48079  dandysum2p2e4  48161  paireqne  48686  sbgoldbo  48978  usgrexmpl1lem  49212  usgrexmpl1tri  49216  usgrexmpl2lem  49217  usgrexmpl2nb0  49222  usgrexmpl2nb2  49224  usgrexmpl2nb3  49225  usgrexmpl2nb4  49226  usgrexmpl2nb5  49227  gpgedg2iv  49258  gpg5nbgrvtx03starlem2  49260  gpg5nbgrvtx13starlem2  49263  gpgprismgr4cycllem2  49287  gpgprismgr4cycllem7  49292  gpg5edgnedg  49321  zlmodzxzldeplem  49703  aacllem  51107