Theorem olci 855

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

Syntax hints:  ¬ wn 3   ∨ wo 836

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 199  df-or 837

This theorem is referenced by:  falortru  1641  opthhausdorff  5214  sucidg  6054  kmlem2  9308  sornom  9434  leid  10472  pnf0xnn0  11721  xrleid  12294  xmul01  12409  bcn1  13418  odd2np1lem  15468  lcm0val  15713  lcmfunsnlem2lem1  15757  lcmfunsnlem2  15759  coprmprod  15780  coprmproddvdslem  15781  prmrec  16030  sratset  19581  srads  19583  m2detleib  20842  zclmncvs  23355  itg0  23983  itgz  23984  coemullem  24443  ftalem5  25255  chp1  25345  prmorcht  25356  pclogsum  25392  logexprlim  25402  bpos1  25460  pntpbnd1  25727  axlowdimlem16  26306  usgrexmpldifpr  26605  cusgrsizeindb1  26798  pthdlem2  27120  ex-or  27853  plymulx0  31224  bj-0eltag  33538  bj-inftyexpidisj  33687  mblfinlem2  34073  volsupnfl  34080  ifpdfor  38767  ifpim1  38771  ifpnot  38772  ifpid2  38773  ifpim2  38774  ifpim1g  38804  ifpbi1b  38806  icccncfext  41028  fourierdlem103  41353  fourierdlem104  41354  etransclem24  41402  etransclem35  41413  abnotataxb  42010  dandysum2p2e4  42092  paireqne  42450  sbgoldbo  42700  zlmodzxzldeplem  43302  line2x  43490  aacllem  43653