Theorem olci 867

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

Syntax hints:  ¬ wn 3   ∨ wo 848

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 207  df-or 849

This theorem is referenced by:  falortru  1581  opthhausdorff  5471  sucidg  6406  f1ounsn  7227  kmlem2  10074  sornom  10199  leid  11242  pnf0xnn0  12517  xrleid  13102  xmul01  13219  bcn1  14275  odd2np1lem  16309  lcm0val  16563  lcmfunsnlem2lem1  16607  lcmfunsnlem2  16609  coprmprod  16630  coprmproddvdslem  16631  prmrec  16893  smndex2dnrinv  18886  m2detleib  22596  zclmncvs  25115  itg0  25747  itgz  25748  coemullem  26215  ftalem5  27040  chp1  27130  prmorcht  27141  pclogsum  27178  logexprlim  27188  bpos1  27246  addsqnreup  27406  pntpbnd1  27549  axlowdimlem16  29026  usgrexmpldifpr  29327  cusgrsizeindb1  29519  pthdlem2  29836  ex-or  30491  ply1coedeg  33649  plymulx0  34691  signstfvn  34713  bj-0eltag  37285  bj-inftyexpidisj  37524  mblfinlem2  37979  volsupnfl  37986  12gcd5e1  42442  ifpdfor  43892  ifpim1  43896  ifpnot  43897  ifpid2  43898  ifpim2  43899  ifpim1g  43928  ifpbi1b  43930  icccncfext  46315  fourierdlem103  46637  fourierdlem104  46638  etransclem24  46686  etransclem35  46697  abnotataxb  47364  dandysum2p2e4  47446  paireqne  47971  sbgoldbo  48263  usgrexmpl1lem  48497  usgrexmpl1tri  48501  usgrexmpl2lem  48502  usgrexmpl2nb0  48507  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  gpgedg2iv  48543  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx13starlem2  48548  gpgprismgr4cycllem2  48572  gpgprismgr4cycllem7  48577  gpg5edgnedg  48606  zlmodzxzldeplem  48974  line2x  49230  aacllem  50276