Theorem orci 861

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

Syntax hints:   ∨ wo 843

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 844

This theorem is referenced by:  truorfal  1577  trunortruOLD  1589  trunorfalOLD  1591  prid1g  4693  isso2i  5529  mpo0v  7337  0wdom  9259  nneo  12334  mnfltpnf  12791  bcpasc  13963  isumless  15485  binomfallfaclem2  15678  lcmfunsnlem2lem1  16271  srabaseOLD  20357  sraaddgOLD  20359  sramulrOLD  20361  m2detleib  21688  fctop  22062  cctop  22064  ovoliunnul  24576  vitalilem5  24681  logtayl  25720  bpos1  26336  usgrexmpldifpr  27528  cffldtocusgr  27717  pthdlem2  28037  inindif  30764  disjunsn  30834  circlemethhgt  32523  fmla0disjsuc  33260  0slt1s  33950  ifpimimb  41009  ifpimim  41014  binomcxplemnn0  41856  binomcxplemnotnn0  41863  salexct  43763  onenotinotbothi  44315  twonotinotbothi  44316  clifte  44317  cliftet  44318  paireqne  44851  sbgoldbo  45127  zlmodzxzldeplem  45727  ldepslinc  45738  line2x  45988  inlinecirc02plem  46020  alimp-surprise  46370  aacllem  46391