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  4762  isso2i  5621  mpo0v  7487  0wdom  9560  nneo  12641  mnfltpnf  13101  bcpasc  14276  isumless  15786  binomfallfaclem2  15979  lcmfunsnlem2lem1  16570  srabaseOLD  20780  sraaddgOLD  20782  sramulrOLD  20784  m2detleib  22114  fctop  22488  cctop  22490  ovoliunnul  25005  vitalilem5  25110  logtayl  26149  bpos1  26765  0slt1s  27309  usgrexmpldifpr  28494  cffldtocusgr  28683  pthdlem2  29004  inindif  31731  disjunsn  31802  circlemethhgt  33592  fmla0disjsuc  34326  disjressuc2  37195  ifpimimb  42187  ifpimim  42192  binomcxplemnn0  43040  binomcxplemnotnn0  43047  salexct  44984  onenotinotbothi  45577  twonotinotbothi  45578  clifte  45579  cliftet  45580  paireqne  46113  sbgoldbo  46389  zlmodzxzldeplem  47080  ldepslinc  47091  line2x  47341  inlinecirc02plem  47373  alimp-surprise  47728  aacllem  47749