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  4704  isso2i  5576  mpo0v  7451  0wdom  9485  nneo  12613  mnfltpnf  13077  bcpasc  14283  isumless  15810  binomfallfaclem2  16005  lcmfunsnlem2lem1  16607  m2detleib  22596  fctop  22969  cctop  22971  ovoliunnul  25474  vitalilem5  25579  logtayl  26624  bpos1  27246  0lt1s  27804  n0s0suc  28334  n0s0m1  28354  nn1m1nns  28366  n0seo  28413  usgrexmpldifpr  29327  cffldtocusgr  29516  pthdlem2  29836  disjunsn  32664  circlemethhgt  34787  fmla0disjsuc  35580  disjressuc2  38732  ifpimimb  43931  ifpimim  43936  binomcxplemnn0  44776  binomcxplemnotnn0  44783  salexct  46762  onenotinotbothi  47381  twonotinotbothi  47382  clifte  47383  cliftet  47384  paireqne  47971  sbgoldbo  48263  usgrexmpl1lem  48497  usgrexmpl1tri  48501  usgrexmpl2lem  48502  usgrexmpl2nb0  48507  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  gpgedg2ov  48542  gpgedg2iv  48543  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpgprismgr4cycllem2  48572  gpgprismgr4cycllem7  48577  gpg5edgnedg  48606  zlmodzxzldeplem  48974  ldepslinc  48985  line2x  49230  inlinecirc02plem  49262  alimp-surprise  50255  aacllem  50276