Theorem olci 865

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

Syntax hints:  ¬ wn 3   ∨ wo 846

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 847

This theorem is referenced by:  falortru  1581  opthhausdorff  5518  sucidg  6446  kmlem2  10146  sornom  10272  leid  11310  pnf0xnn0  12551  xrleid  13130  xmul01  13246  bcn1  14273  odd2np1lem  16283  lcm0val  16531  lcmfunsnlem2lem1  16575  lcmfunsnlem2  16577  coprmprod  16598  coprmproddvdslem  16599  prmrec  16855  smndex2dnrinv  18796  sratsetOLD  20804  sradsOLD  20807  m2detleib  22133  zclmncvs  24665  itg0  25297  itgz  25298  coemullem  25764  ftalem5  26581  chp1  26671  prmorcht  26682  pclogsum  26718  logexprlim  26728  bpos1  26786  addsqnreup  26946  pntpbnd1  27089  axlowdimlem16  28215  usgrexmpldifpr  28515  cusgrsizeindb1  28707  pthdlem2  29025  ex-or  29674  plymulx0  33558  signstfvn  33580  bj-0eltag  35859  bj-inftyexpidisj  36091  mblfinlem2  36526  volsupnfl  36533  12gcd5e1  40868  ifpdfor  42216  ifpim1  42220  ifpnot  42221  ifpid2  42222  ifpim2  42223  ifpim1g  42252  ifpbi1b  42254  icccncfext  44603  fourierdlem103  44925  fourierdlem104  44926  etransclem24  44974  etransclem35  44985  abnotataxb  45626  dandysum2p2e4  45708  paireqne  46179  sbgoldbo  46455  zlmodzxzldeplem  47179  line2x  47440  aacllem  47848