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  4724  isso2i  5583  mpo0v  7473  0wdom  9523  nneo  12618  mnfltpnf  13086  bcpasc  14286  isumless  15811  binomfallfaclem2  16006  lcmfunsnlem2lem1  16608  m2detleib  22518  fctop  22891  cctop  22893  ovoliunnul  25408  vitalilem5  25513  logtayl  26569  bpos1  27194  0slt1s  27741  n0s0suc  28234  n0s0m1  28252  nn1m1nns  28263  n0seo  28307  usgrexmpldifpr  29185  cffldtocusgr  29374  cffldtocusgrOLD  29375  pthdlem2  29698  disjunsn  32523  circlemethhgt  34634  fmla0disjsuc  35385  disjressuc2  38374  ifpimimb  43493  ifpimim  43498  binomcxplemnn0  44338  binomcxplemnotnn0  44345  salexct  46332  onenotinotbothi  46934  twonotinotbothi  46935  clifte  46936  cliftet  46937  paireqne  47512  sbgoldbo  47788  usgrexmpl1lem  48012  usgrexmpl1tri  48016  usgrexmpl2lem  48017  usgrexmpl2nb0  48022  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  gpgedg2ov  48057  gpgedg2iv  48058  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  gpgprismgr4cycllem2  48086  gpgprismgr4cycllem7  48091  zlmodzxzldeplem  48487  ldepslinc  48498  line2x  48743  inlinecirc02plem  48775  alimp-surprise  49769  aacllem  49790