Theorem olci 866

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

Syntax hints:  ¬ wn 3   ∨ wo 847

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 848

This theorem is referenced by:  falortru  1580  opthhausdorff  5457  sucidg  6389  f1ounsn  7206  kmlem2  10040  sornom  10165  leid  11206  pnf0xnn0  12458  xrleid  13047  xmul01  13163  bcn1  14217  odd2np1lem  16248  lcm0val  16502  lcmfunsnlem2lem1  16546  lcmfunsnlem2  16548  coprmprod  16569  coprmproddvdslem  16570  prmrec  16831  smndex2dnrinv  18820  m2detleib  22544  zclmncvs  25073  itg0  25706  itgz  25707  coemullem  26180  ftalem5  27012  chp1  27102  prmorcht  27113  pclogsum  27151  logexprlim  27161  bpos1  27219  addsqnreup  27379  pntpbnd1  27522  axlowdimlem16  28933  usgrexmpldifpr  29234  cusgrsizeindb1  29427  pthdlem2  29744  ex-or  30396  plymulx0  34555  signstfvn  34577  bj-0eltag  37011  bj-inftyexpidisj  37243  mblfinlem2  37697  volsupnfl  37704  12gcd5e1  42035  ifpdfor  43497  ifpim1  43501  ifpnot  43502  ifpid2  43503  ifpim2  43504  ifpim1g  43533  ifpbi1b  43535  icccncfext  45924  fourierdlem103  46246  fourierdlem104  46247  etransclem24  46295  etransclem35  46306  abnotataxb  46946  dandysum2p2e4  47028  paireqne  47541  sbgoldbo  47817  usgrexmpl1lem  48051  usgrexmpl1tri  48055  usgrexmpl2lem  48056  usgrexmpl2nb0  48061  usgrexmpl2nb2  48063  usgrexmpl2nb3  48064  usgrexmpl2nb4  48065  usgrexmpl2nb5  48066  gpgedg2iv  48097  gpg5nbgrvtx03starlem2  48099  gpg5nbgrvtx13starlem2  48102  gpgprismgr4cycllem2  48126  gpgprismgr4cycllem7  48131  gpg5edgnedg  48160  zlmodzxzldeplem  48529  line2x  48785  aacllem  49832