Theorem orci 862

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

Syntax hints:   ∨ wo 844

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 845

This theorem is referenced by:  truorfal  1576  trunortruOLD  1588  trunorfalOLD  1590  prid1g  4656  isso2i  5472  mpo0v  7217  0wdom  9018  nneo  12054  mnfltpnf  12509  bcpasc  13677  isumless  15192  binomfallfaclem2  15386  lcmfunsnlem2lem1  15972  srabase  19943  sraaddg  19944  sramulr  19945  m2detleib  21236  fctop  21609  cctop  21611  ovoliunnul  24111  vitalilem5  24216  logtayl  25251  bpos1  25867  usgrexmpldifpr  27048  cffldtocusgr  27237  pthdlem2  27557  inindif  30287  disjunsn  30357  circlemethhgt  32024  fmla0disjsuc  32758  ifpimimb  40212  ifpimim  40217  binomcxplemnn0  41053  binomcxplemnotnn0  41060  salexct  42974  onenotinotbothi  43526  twonotinotbothi  43527  clifte  43528  cliftet  43529  paireqne  44028  sbgoldbo  44305  zlmodzxzldeplem  44907  ldepslinc  44918  line2x  45168  inlinecirc02plem  45200  alimp-surprise  45308  aacllem  45329