Theorem orci 866

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

Syntax hints:   ∨ wo 848

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 849

This theorem is referenced by:  truorfal  1580  prid1g  4719  isso2i  5577  mpo0v  7452  0wdom  9487  nneo  12588  mnfltpnf  13052  bcpasc  14256  isumless  15780  binomfallfaclem2  15975  lcmfunsnlem2lem1  16577  m2detleib  22587  fctop  22960  cctop  22962  ovoliunnul  25476  vitalilem5  25581  logtayl  26637  bpos1  27262  0lt1s  27820  n0s0suc  28350  n0s0m1  28370  nn1m1nns  28382  n0seo  28429  usgrexmpldifpr  29343  cffldtocusgr  29532  cffldtocusgrOLD  29533  pthdlem2  29853  disjunsn  32680  circlemethhgt  34820  fmla0disjsuc  35611  disjressuc2  38656  ifpimimb  43854  ifpimim  43859  binomcxplemnn0  44699  binomcxplemnotnn0  44706  salexct  46686  onenotinotbothi  47287  twonotinotbothi  47288  clifte  47289  cliftet  47290  paireqne  47865  sbgoldbo  48141  usgrexmpl1lem  48375  usgrexmpl1tri  48379  usgrexmpl2lem  48380  usgrexmpl2nb0  48385  usgrexmpl2nb1  48386  usgrexmpl2nb2  48387  usgrexmpl2nb3  48388  usgrexmpl2nb4  48389  usgrexmpl2nb5  48390  gpgedg2ov  48420  gpgedg2iv  48421  gpg5nbgrvtx03starlem1  48422  gpg5nbgrvtx03starlem2  48423  gpg5nbgrvtx03starlem3  48424  gpg5nbgrvtx13starlem1  48425  gpg5nbgrvtx13starlem2  48426  gpg5nbgrvtx13starlem3  48427  gpgprismgr4cycllem2  48450  gpgprismgr4cycllem7  48455  gpg5edgnedg  48484  zlmodzxzldeplem  48852  ldepslinc  48863  line2x  49108  inlinecirc02plem  49140  alimp-surprise  50133  aacllem  50154