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  5490  sucidg  6439  f1ounsn  7272  kmlem2  10211  sornom  10336  leid  11387  pnf0xnn0  12667  xrleid  13261  xmul01  13378  bcn1  14437  odd2np1lem  16490  lcm0val  16749  lcmfunsnlem2lem1  16793  lcmfunsnlem2  16795  coprmprod  16816  coprmproddvdslem  16817  prmrec  17080  smndex2dnrinv  19094  degenmgm  19117  degenmgm2  19120  m2detleib  22926  zclmncvs  25449  itg0  26080  itgz  26081  coemullem  26549  plyn0mulidp  26584  ftalem5  27386  chp1  27476  prmorcht  27487  pclogsum  27524  logexprlim  27534  bpos1  27592  addsqnreup  27752  pntpbnd1  27895  axlowdimlem16  29517  usgrexmpldifpr  29821  cusgrsizeindb1  30013  pthdlem2  30336  ex-or  31004  ply1coedeg  34103  signstfvn  35181  bj-0eltag  37861  bj-inftyexpidisj  38099  mblfinlem2  38544  volsupnfl  38551  12gcd5e1  43021  ifpdfor  44424  ifpim1  44428  ifpnot  44429  ifpid2  44430  ifpim2  44431  ifpim1g  44460  ifpbi1b  44462  icccncfext  46841  fourierdlem103  47163  fourierdlem104  47164  etransclem24  47212  etransclem35  47223  abnotataxb  47930  dandysum2p2e4  48012  paireqne  48537  sbgoldbo  48829  usgrexmpl1lem  49063  usgrexmpl1tri  49067  usgrexmpl2lem  49068  usgrexmpl2nb0  49073  usgrexmpl2nb2  49075  usgrexmpl2nb3  49076  usgrexmpl2nb4  49077  usgrexmpl2nb5  49078  gpgedg2iv  49109  gpg5nbgrvtx03starlem2  49111  gpg5nbgrvtx13starlem2  49114  gpgprismgr4cycllem2  49138  gpgprismgr4cycllem7  49143  gpg5edgnedg  49172  zlmodzxzldeplem  49554  line2x  49810  aacllem  50883