Theorem orci 876

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

Syntax hints:   ∨ wo 858

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 209  df-or 859

This theorem is referenced by:  truorfal  1597  prid1g  4718  isso2i  5590  mpo0v  7476  0wdom  9515  nneo  12654  mnfltpnf  13125  bcpasc  14331  isumless  15858  binomfallfaclem2  16053  lcmfunsnlem2lem1  16655  m2detleib  22671  fctop  23044  cctop  23046  ovoliunnul  25549  vitalilem5  25654  logtayl  26702  bpos1  27324  0lt1s  27882  n0s0suc  28412  n0s0m1  28432  nn1m1nns  28444  n0seo  28491  usgrexmpldifpr  29405  cffldtocusgr  29594  pthdlem2  29914  disjunsn  32743  circlemethhgt  34901  fmla0disjsuc  35712  disjressuc2  38874  ifpimimb  44044  ifpimim  44049  binomcxplemnn0  44889  binomcxplemnotnn0  44896  salexct  46872  onenotinotbothi  47491  twonotinotbothi  47492  clifte  47493  cliftet  47494  paireqne  48081  sbgoldbo  48373  usgrexmpl1lem  48607  usgrexmpl1tri  48611  usgrexmpl2lem  48612  usgrexmpl2nb0  48617  usgrexmpl2nb1  48618  usgrexmpl2nb2  48619  usgrexmpl2nb3  48620  usgrexmpl2nb4  48621  usgrexmpl2nb5  48622  gpgedg2ov  48652  gpgedg2iv  48653  gpg5nbgrvtx03starlem1  48654  gpg5nbgrvtx03starlem2  48655  gpg5nbgrvtx03starlem3  48656  gpg5nbgrvtx13starlem1  48657  gpg5nbgrvtx13starlem2  48658  gpg5nbgrvtx13starlem3  48659  gpgprismgr4cycllem2  48682  gpgprismgr4cycllem7  48687  gpg5edgnedg  48716  zlmodzxzldeplem  49084  ldepslinc  49095  line2x  49340  inlinecirc02plem  49372  alimp-surprise  50365  aacllem  50386