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

This theorem is referenced by:  truorfal  1575  prid1g  4785  isso2i  5644  mpo0v  7534  0wdom  9639  nneo  12727  mnfltpnf  13189  bcpasc  14370  isumless  15893  binomfallfaclem2  16088  lcmfunsnlem2lem1  16685  srabaseOLD  21201  sraaddgOLD  21203  sramulrOLD  21205  m2detleib  22658  fctop  23032  cctop  23034  ovoliunnul  25561  vitalilem5  25666  logtayl  26720  bpos1  27345  0slt1s  27892  n0s0suc  28363  n0s0m1  28377  n0seo  28423  nohalf  28425  usgrexmpldifpr  29293  cffldtocusgr  29482  cffldtocusgrOLD  29483  pthdlem2  29804  inindif  32546  disjunsn  32616  circlemethhgt  34620  fmla0disjsuc  35366  disjressuc2  38344  ifpimimb  43466  ifpimim  43471  binomcxplemnn0  44318  binomcxplemnotnn0  44325  salexct  46255  onenotinotbothi  46848  twonotinotbothi  46849  clifte  46850  cliftet  46851  paireqne  47385  sbgoldbo  47661  usgrexmpl1lem  47836  usgrexmpl1tri  47840  usgrexmpl2lem  47841  usgrexmpl2nb0  47846  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  zlmodzxzldeplem  48227  ldepslinc  48238  line2x  48488  inlinecirc02plem  48520  alimp-surprise  48874  aacllem  48895