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  4712  isso2i  5564  mpo0v  7436  0wdom  9463  nneo  12563  mnfltpnf  13027  bcpasc  14230  isumless  15754  binomfallfaclem2  15949  lcmfunsnlem2lem1  16551  m2detleib  22547  fctop  22920  cctop  22922  ovoliunnul  25436  vitalilem5  25541  logtayl  26597  bpos1  27222  0slt1s  27774  n0s0suc  28271  n0s0m1  28289  nn1m1nns  28300  n0seo  28345  usgrexmpldifpr  29238  cffldtocusgr  29427  cffldtocusgrOLD  29428  pthdlem2  29748  disjunsn  32576  circlemethhgt  34677  fmla0disjsuc  35463  disjressuc2  38455  ifpimimb  43621  ifpimim  43626  binomcxplemnn0  44466  binomcxplemnotnn0  44473  salexct  46456  onenotinotbothi  47057  twonotinotbothi  47058  clifte  47059  cliftet  47060  paireqne  47635  sbgoldbo  47911  usgrexmpl1lem  48145  usgrexmpl1tri  48149  usgrexmpl2lem  48150  usgrexmpl2nb0  48155  usgrexmpl2nb1  48156  usgrexmpl2nb2  48157  usgrexmpl2nb3  48158  usgrexmpl2nb4  48159  usgrexmpl2nb5  48160  gpgedg2ov  48190  gpgedg2iv  48191  gpg5nbgrvtx03starlem1  48192  gpg5nbgrvtx03starlem2  48193  gpg5nbgrvtx03starlem3  48194  gpg5nbgrvtx13starlem1  48195  gpg5nbgrvtx13starlem2  48196  gpg5nbgrvtx13starlem3  48197  gpgprismgr4cycllem2  48220  gpgprismgr4cycllem7  48225  gpg5edgnedg  48254  zlmodzxzldeplem  48623  ldepslinc  48634  line2x  48879  inlinecirc02plem  48911  alimp-surprise  49905  aacllem  49926