Theorem orci 865

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

Proof of Theorem orci

Step	Hyp	Ref	Expression
1		orci.1	. . 3 ⊢ 𝜑
2	1	pm2.24i 150	. 2 ⊢ (¬ 𝜑 → 𝜓)
3	2	orri 862	1 ⊢ (𝜑 ∨ 𝜓)

Syntax hints:   ∨ 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:  truorfal  1575  prid1g  4765  isso2i  5633  mpo0v  7517  0wdom  9608  nneo  12700  mnfltpnf  13166  bcpasc  14357  isumless  15878  binomfallfaclem2  16073  lcmfunsnlem2lem1  16672  srabaseOLD  21196  sraaddgOLD  21198  sramulrOLD  21200  m2detleib  22653  fctop  23027  cctop  23029  ovoliunnul  25556  vitalilem5  25661  logtayl  26717  bpos1  27342  0slt1s  27889  n0s0suc  28360  n0s0m1  28374  n0seo  28420  nohalf  28422  usgrexmpldifpr  29290  cffldtocusgr  29479  cffldtocusgrOLD  29480  pthdlem2  29801  disjunsn  32614  circlemethhgt  34637  fmla0disjsuc  35383  disjressuc2  38370  ifpimimb  43494  ifpimim  43499  binomcxplemnn0  44345  binomcxplemnotnn0  44352  salexct  46290  onenotinotbothi  46883  twonotinotbothi  46884  clifte  46885  cliftet  46886  paireqne  47436  sbgoldbo  47712  usgrexmpl1lem  47916  usgrexmpl1tri  47920  usgrexmpl2lem  47921  usgrexmpl2nb0  47926  usgrexmpl2nb1  47927  usgrexmpl2nb2  47928  usgrexmpl2nb3  47929  usgrexmpl2nb4  47930  usgrexmpl2nb5  47931  gpg5nbgrvtx03starlem1  47959  gpg5nbgrvtx03starlem2  47960  gpg5nbgrvtx03starlem3  47961  gpg5nbgrvtx13starlem1  47962  gpg5nbgrvtx13starlem2  47963  gpg5nbgrvtx13starlem3  47964  zlmodzxzldeplem  48344  ldepslinc  48355  line2x  48604  inlinecirc02plem  48636  alimp-surprise  49011  aacllem  49032