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 153	. 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 210  df-or 847

This theorem is referenced by:  truorfal  1580  trunortruOLD  1592  trunorfalOLD  1594  prid1g  4651  isso2i  5477  mpo0v  7252  0wdom  9107  nneo  12147  mnfltpnf  12604  bcpasc  13773  isumless  15293  binomfallfaclem2  15486  lcmfunsnlem2lem1  16079  srabase  20069  sraaddg  20070  sramulr  20071  m2detleib  21382  fctop  21755  cctop  21757  ovoliunnul  24259  vitalilem5  24364  logtayl  25403  bpos1  26019  usgrexmpldifpr  27200  cffldtocusgr  27389  pthdlem2  27709  inindif  30437  disjunsn  30507  circlemethhgt  32193  fmla0disjsuc  32931  0slt1s  33664  ifpimimb  40665  ifpimim  40670  binomcxplemnn0  41505  binomcxplemnotnn0  41512  salexct  43415  onenotinotbothi  43967  twonotinotbothi  43968  clifte  43969  cliftet  43970  paireqne  44497  sbgoldbo  44773  zlmodzxzldeplem  45373  ldepslinc  45384  line2x  45634  inlinecirc02plem  45666  alimp-surprise  45937  aacllem  45958