Theorem olci 864

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

Syntax hints:  ¬ wn 3   ∨ wo 845

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 206  df-or 846

This theorem is referenced by:  falortru  1580  opthhausdorff  5516  sucidg  6442  kmlem2  10142  sornom  10268  leid  11306  pnf0xnn0  12547  xrleid  13126  xmul01  13242  bcn1  14269  odd2np1lem  16279  lcm0val  16527  lcmfunsnlem2lem1  16571  lcmfunsnlem2  16573  coprmprod  16594  coprmproddvdslem  16595  prmrec  16851  smndex2dnrinv  18792  sratsetOLD  20796  sradsOLD  20799  m2detleib  22124  zclmncvs  24656  itg0  25288  itgz  25289  coemullem  25755  ftalem5  26570  chp1  26660  prmorcht  26671  pclogsum  26707  logexprlim  26717  bpos1  26775  addsqnreup  26935  pntpbnd1  27078  axlowdimlem16  28204  usgrexmpldifpr  28504  cusgrsizeindb1  28696  pthdlem2  29014  ex-or  29663  plymulx0  33546  signstfvn  33568  bj-0eltag  35847  bj-inftyexpidisj  36079  mblfinlem2  36514  volsupnfl  36521  12gcd5e1  40856  ifpdfor  42201  ifpim1  42205  ifpnot  42206  ifpid2  42207  ifpim2  42208  ifpim1g  42237  ifpbi1b  42239  icccncfext  44589  fourierdlem103  44911  fourierdlem104  44912  etransclem24  44960  etransclem35  44971  abnotataxb  45612  dandysum2p2e4  45694  paireqne  46165  sbgoldbo  46441  zlmodzxzldeplem  47132  line2x  47393  aacllem  47801