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  5407  sucidg  6269  kmlem2  9577  sornom  9699  leid  10736  pnf0xnn0  11975  xrleid  12545  xmul01  12661  bcn1  13674  odd2np1lem  15689  lcm0val  15938  lcmfunsnlem2lem1  15982  lcmfunsnlem2  15984  coprmprod  16005  coprmproddvdslem  16006  prmrec  16258  smndex2dnrinv  18080  sratset  19956  srads  19958  m2detleib  21240  zclmncvs  23752  itg0  24380  itgz  24381  coemullem  24840  ftalem5  25654  chp1  25744  prmorcht  25755  pclogsum  25791  logexprlim  25801  bpos1  25859  addsqnreup  26019  pntpbnd1  26162  axlowdimlem16  26743  usgrexmpldifpr  27040  cusgrsizeindb1  27232  pthdlem2  27549  ex-or  28200  plymulx0  31817  signstfvn  31839  bj-0eltag  34293  bj-inftyexpidisj  34495  mblfinlem2  34945  volsupnfl  34952  ifpdfor  39850  ifpim1  39854  ifpnot  39855  ifpid2  39856  ifpim2  39857  ifpim1g  39887  ifpbi1b  39889  icccncfext  42190  fourierdlem103  42514  fourierdlem104  42515  etransclem24  42563  etransclem35  42574  abnotataxb  43172  dandysum2p2e4  43254  paireqne  43693  sbgoldbo  43972  zlmodzxzldeplem  44573  line2x  44761  aacllem  44922