Theorem olci 880

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

This proof depends on syntax axioms:  ¬ wn 3   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  falortru  1609  opthhausdorff  5495  sucidg  6467  f1ounsn  7306  kmlem2  10260  sornom  10385  leid  11436  pnf0xnn0  12716  xrleid  13310  xmul01  13427  bcn1  14487  odd2np1lem  16542  lcm0val  16801  lcmfunsnlem2lem1  16845  lcmfunsnlem2  16847  coprmprod  16868  coprmproddvdslem  16869  prmrec  17132  smndex2dnrinv  19146  degenmgm  19169  degenmgm2  19172  m2detleib  22979  zclmncvs  25502  itg0  26133  itgz  26134  coemullem  26602  plyn0mulidp  26635  ftalem5  27437  chp1  27527  prmorcht  27538  pclogsum  27575  logexprlim  27585  bpos1  27643  addsqnreup  27803  pntpbnd1  27946  axlowdimlem16  29568  usgrexmpldifpr  29872  cusgrsizeindb1  30064  pthdlem2  30387  ex-or  31055  ply1coedeg  34204  signstfvn  35281  bj-0eltag  38082  bj-inftyexpidisj  38336  mblfinlem2  38781  volsupnfl  38788  12gcd5e1  43256  ifpdfor  44669  ifpim1  44673  ifpnot  44674  ifpid2  44675  ifpim2  44676  ifpim1g  44705  ifpbi1b  44707  icccncfext  47112  fourierdlem103  47434  fourierdlem104  47435  etransclem24  47483  etransclem35  47494  abnotataxb  48201  dandysum2p2e4  48283  paireqne  48808  sbgoldbo  49100  usgrexmpl1lem  49334  usgrexmpl1tri  49338  usgrexmpl2lem  49339  usgrexmpl2nb0  49344  usgrexmpl2nb2  49346  usgrexmpl2nb3  49347  usgrexmpl2nb4  49348  usgrexmpl2nb5  49349  gpgedg2iv  49380  gpg5nbgrvtx03starlem2  49382  gpg5nbgrvtx13starlem2  49385  gpgprismgr4cycllem2  49409  gpgprismgr4cycllem7  49414  gpg5edgnedg  49443  zlmodzxzldeplem  49825  aacllem  51251