Theorem orci 864

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 861	1 ⊢ (𝜑 ∨ 𝜓)

Syntax hints:   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  truorfal  1580  prid1g  4765  isso2i  5624  mpo0v  7493  0wdom  9565  nneo  12646  mnfltpnf  13106  bcpasc  14281  isumless  15791  binomfallfaclem2  15984  lcmfunsnlem2lem1  16575  srabaseOLD  20793  sraaddgOLD  20795  sramulrOLD  20797  m2detleib  22133  fctop  22507  cctop  22509  ovoliunnul  25024  vitalilem5  25129  logtayl  26168  bpos1  26786  0slt1s  27330  usgrexmpldifpr  28515  cffldtocusgr  28704  pthdlem2  29025  inindif  31754  disjunsn  31825  circlemethhgt  33655  fmla0disjsuc  34389  disjressuc2  37258  ifpimimb  42255  ifpimim  42260  binomcxplemnn0  43108  binomcxplemnotnn0  43115  salexct  45050  onenotinotbothi  45643  twonotinotbothi  45644  clifte  45645  cliftet  45646  paireqne  46179  sbgoldbo  46455  zlmodzxzldeplem  47179  ldepslinc  47190  line2x  47440  inlinecirc02plem  47472  alimp-surprise  47827  aacllem  47848