Theorem olci 862

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

Syntax hints:  ¬ wn 3   ∨ wo 843

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 209  df-or 844

This theorem is referenced by:  falortru  1576  opthhausdorff  5409  sucidg  6271  kmlem2  9579  sornom  9701  leid  10738  pnf0xnn0  11977  xrleid  12547  xmul01  12663  bcn1  13676  odd2np1lem  15691  lcm0val  15940  lcmfunsnlem2lem1  15984  lcmfunsnlem2  15986  coprmprod  16007  coprmproddvdslem  16008  prmrec  16260  smndex2dnrinv  18082  sratset  19958  srads  19960  m2detleib  21242  zclmncvs  23754  itg0  24382  itgz  24383  coemullem  24842  ftalem5  25656  chp1  25746  prmorcht  25757  pclogsum  25793  logexprlim  25803  bpos1  25861  addsqnreup  26021  pntpbnd1  26164  axlowdimlem16  26745  usgrexmpldifpr  27042  cusgrsizeindb1  27234  pthdlem2  27551  ex-or  28202  plymulx0  31819  signstfvn  31841  bj-0eltag  34292  bj-inftyexpidisj  34494  mblfinlem2  34932  volsupnfl  34939  ifpdfor  39837  ifpim1  39841  ifpnot  39842  ifpid2  39843  ifpim2  39844  ifpim1g  39874  ifpbi1b  39876  icccncfext  42177  fourierdlem103  42501  fourierdlem104  42502  etransclem24  42550  etransclem35  42561  abnotataxb  43159  dandysum2p2e4  43241  paireqne  43680  sbgoldbo  43959  zlmodzxzldeplem  44560  line2x  44748  aacllem  44909