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  1579  prid1g  4717  isso2i  5569  mpo0v  7442  0wdom  9475  nneo  12576  mnfltpnf  13040  bcpasc  14244  isumless  15768  binomfallfaclem2  15963  lcmfunsnlem2lem1  16565  m2detleib  22575  fctop  22948  cctop  22950  ovoliunnul  25464  vitalilem5  25569  logtayl  26625  bpos1  27250  0lt1s  27808  n0s0suc  28338  n0s0m1  28358  nn1m1nns  28370  n0seo  28417  usgrexmpldifpr  29331  cffldtocusgr  29520  cffldtocusgrOLD  29521  pthdlem2  29841  disjunsn  32669  circlemethhgt  34800  fmla0disjsuc  35592  disjressuc2  38592  ifpimimb  43741  ifpimim  43746  binomcxplemnn0  44586  binomcxplemnotnn0  44593  salexct  46574  onenotinotbothi  47175  twonotinotbothi  47176  clifte  47177  cliftet  47178  paireqne  47753  sbgoldbo  48029  usgrexmpl1lem  48263  usgrexmpl1tri  48267  usgrexmpl2lem  48268  usgrexmpl2nb0  48273  usgrexmpl2nb1  48274  usgrexmpl2nb2  48275  usgrexmpl2nb3  48276  usgrexmpl2nb4  48277  usgrexmpl2nb5  48278  gpgedg2ov  48308  gpgedg2iv  48309  gpg5nbgrvtx03starlem1  48310  gpg5nbgrvtx03starlem2  48311  gpg5nbgrvtx03starlem3  48312  gpg5nbgrvtx13starlem1  48313  gpg5nbgrvtx13starlem2  48314  gpg5nbgrvtx13starlem3  48315  gpgprismgr4cycllem2  48338  gpgprismgr4cycllem7  48343  gpg5edgnedg  48372  zlmodzxzldeplem  48740  ldepslinc  48751  line2x  48996  inlinecirc02plem  49028  alimp-surprise  50021  aacllem  50042