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  5498  sucidg  6445  f1ounsn  7277  kmlem2  10158  sornom  10283  leid  11334  pnf0xnn0  12612  xrleid  13206  xmul01  13323  bcn1  14381  odd2np1lem  16436  lcm0val  16690  lcmfunsnlem2lem1  16734  lcmfunsnlem2  16736  coprmprod  16757  coprmproddvdslem  16758  prmrec  17020  smndex2dnrinv  19033  degenmgm  19056  degenmgm2  19059  m2detleib  22859  zclmncvs  25382  itg0  26014  itgz  26015  coemullem  26483  plyn0mulidp  26518  ftalem5  27321  chp1  27411  prmorcht  27422  pclogsum  27459  logexprlim  27469  bpos1  27527  addsqnreup  27687  pntpbnd1  27830  axlowdimlem16  29422  usgrexmpldifpr  29726  cusgrsizeindb1  29918  pthdlem2  30241  ex-or  30909  ply1coedeg  34007  signstfvn  35085  bj-0eltag  37730  bj-inftyexpidisj  37970  mblfinlem2  38415  volsupnfl  38422  12gcd5e1  42877  ifpdfor  44313  ifpim1  44317  ifpnot  44318  ifpid2  44319  ifpim2  44320  ifpim1g  44349  ifpbi1b  44351  icccncfext  46723  fourierdlem103  47045  fourierdlem104  47046  etransclem24  47094  etransclem35  47105  abnotataxb  47812  dandysum2p2e4  47894  paireqne  48419  sbgoldbo  48711  usgrexmpl1lem  48945  usgrexmpl1tri  48949  usgrexmpl2lem  48950  usgrexmpl2nb0  48955  usgrexmpl2nb2  48957  usgrexmpl2nb3  48958  usgrexmpl2nb4  48959  usgrexmpl2nb5  48960  gpgedg2iv  48991  gpg5nbgrvtx03starlem2  48993  gpg5nbgrvtx13starlem2  48996  gpgprismgr4cycllem2  49020  gpgprismgr4cycllem7  49025  gpg5edgnedg  49054  zlmodzxzldeplem  49436  line2x  49692  aacllem  50780