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  4705  isso2i  5567  mpo0v  7442  0wdom  9476  nneo  12577  mnfltpnf  13041  bcpasc  14245  isumless  15769  binomfallfaclem2  15964  lcmfunsnlem2lem1  16566  m2detleib  22574  fctop  22947  cctop  22949  ovoliunnul  25452  vitalilem5  25557  logtayl  26609  bpos1  27234  0lt1s  27792  n0s0suc  28322  n0s0m1  28342  nn1m1nns  28354  n0seo  28401  usgrexmpldifpr  29315  cffldtocusgr  29504  cffldtocusgrOLD  29505  pthdlem2  29825  disjunsn  32653  circlemethhgt  34793  fmla0disjsuc  35586  disjressuc2  38723  ifpimimb  43934  ifpimim  43939  binomcxplemnn0  44779  binomcxplemnotnn0  44786  salexct  46766  onenotinotbothi  47367  twonotinotbothi  47368  clifte  47369  cliftet  47370  paireqne  47945  sbgoldbo  48221  usgrexmpl1lem  48455  usgrexmpl1tri  48459  usgrexmpl2lem  48460  usgrexmpl2nb0  48465  usgrexmpl2nb1  48466  usgrexmpl2nb2  48467  usgrexmpl2nb3  48468  usgrexmpl2nb4  48469  usgrexmpl2nb5  48470  gpgedg2ov  48500  gpgedg2iv  48501  gpg5nbgrvtx03starlem1  48502  gpg5nbgrvtx03starlem2  48503  gpg5nbgrvtx03starlem3  48504  gpg5nbgrvtx13starlem1  48505  gpg5nbgrvtx13starlem2  48506  gpg5nbgrvtx13starlem3  48507  gpgprismgr4cycllem2  48530  gpgprismgr4cycllem7  48535  gpg5edgnedg  48564  zlmodzxzldeplem  48932  ldepslinc  48943  line2x  49188  inlinecirc02plem  49220  alimp-surprise  50213  aacllem  50234