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  4713  isso2i  5561  mpo0v  7430  0wdom  9456  nneo  12554  mnfltpnf  13022  bcpasc  14225  isumless  15749  binomfallfaclem2  15944  lcmfunsnlem2lem1  16546  m2detleib  22544  fctop  22917  cctop  22919  ovoliunnul  25433  vitalilem5  25538  logtayl  26594  bpos1  27219  0slt1s  27771  n0s0suc  28268  n0s0m1  28286  nn1m1nns  28297  n0seo  28342  usgrexmpldifpr  29234  cffldtocusgr  29423  cffldtocusgrOLD  29424  pthdlem2  29744  disjunsn  32569  circlemethhgt  34651  fmla0disjsuc  35430  disjressuc2  38419  ifpimimb  43536  ifpimim  43541  binomcxplemnn0  44381  binomcxplemnotnn0  44388  salexct  46371  onenotinotbothi  46963  twonotinotbothi  46964  clifte  46965  cliftet  46966  paireqne  47541  sbgoldbo  47817  usgrexmpl1lem  48051  usgrexmpl1tri  48055  usgrexmpl2lem  48056  usgrexmpl2nb0  48061  usgrexmpl2nb1  48062  usgrexmpl2nb2  48063  usgrexmpl2nb3  48064  usgrexmpl2nb4  48065  usgrexmpl2nb5  48066  gpgedg2ov  48096  gpgedg2iv  48097  gpg5nbgrvtx03starlem1  48098  gpg5nbgrvtx03starlem2  48099  gpg5nbgrvtx03starlem3  48100  gpg5nbgrvtx13starlem1  48101  gpg5nbgrvtx13starlem2  48102  gpg5nbgrvtx13starlem3  48103  gpgprismgr4cycllem2  48126  gpgprismgr4cycllem7  48131  gpg5edgnedg  48160  zlmodzxzldeplem  48529  ldepslinc  48540  line2x  48785  inlinecirc02plem  48817  alimp-surprise  49811  aacllem  49832