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  1578  prid1g  4727  isso2i  5586  mpo0v  7476  0wdom  9530  nneo  12625  mnfltpnf  13093  bcpasc  14293  isumless  15818  binomfallfaclem2  16013  lcmfunsnlem2lem1  16615  m2detleib  22525  fctop  22898  cctop  22900  ovoliunnul  25415  vitalilem5  25520  logtayl  26576  bpos1  27201  0slt1s  27748  n0s0suc  28241  n0s0m1  28259  nn1m1nns  28270  n0seo  28314  usgrexmpldifpr  29192  cffldtocusgr  29381  cffldtocusgrOLD  29382  pthdlem2  29705  disjunsn  32530  circlemethhgt  34641  fmla0disjsuc  35392  disjressuc2  38381  ifpimimb  43500  ifpimim  43505  binomcxplemnn0  44345  binomcxplemnotnn0  44352  salexct  46339  onenotinotbothi  46938  twonotinotbothi  46939  clifte  46940  cliftet  46941  paireqne  47516  sbgoldbo  47792  usgrexmpl1lem  48016  usgrexmpl1tri  48020  usgrexmpl2lem  48021  usgrexmpl2nb0  48026  usgrexmpl2nb1  48027  usgrexmpl2nb2  48028  usgrexmpl2nb3  48029  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  gpgedg2ov  48061  gpgedg2iv  48062  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  gpgprismgr4cycllem2  48090  gpgprismgr4cycllem7  48095  zlmodzxzldeplem  48491  ldepslinc  48502  line2x  48747  inlinecirc02plem  48779  alimp-surprise  49773  aacllem  49794