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  1578  prid1g  4760  isso2i  5629  mpo0v  7517  0wdom  9610  nneo  12702  mnfltpnf  13168  bcpasc  14360  isumless  15881  binomfallfaclem2  16076  lcmfunsnlem2lem1  16675  srabaseOLD  21178  sraaddgOLD  21180  sramulrOLD  21182  m2detleib  22637  fctop  23011  cctop  23013  ovoliunnul  25542  vitalilem5  25647  logtayl  26702  bpos1  27327  0slt1s  27874  n0s0suc  28345  n0s0m1  28359  n0seo  28405  nohalf  28407  usgrexmpldifpr  29275  cffldtocusgr  29464  cffldtocusgrOLD  29465  pthdlem2  29788  disjunsn  32607  circlemethhgt  34658  fmla0disjsuc  35403  disjressuc2  38389  ifpimimb  43517  ifpimim  43522  binomcxplemnn0  44368  binomcxplemnotnn0  44375  salexct  46349  onenotinotbothi  46945  twonotinotbothi  46946  clifte  46947  cliftet  46948  paireqne  47498  sbgoldbo  47774  usgrexmpl1lem  47980  usgrexmpl1tri  47984  usgrexmpl2lem  47985  usgrexmpl2nb0  47990  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  zlmodzxzldeplem  48415  ldepslinc  48426  line2x  48675  inlinecirc02plem  48707  alimp-surprise  49299  aacllem  49320