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 150	. 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 206  df-or 845

This theorem is referenced by:  truorfal  1577  trunorfalOLD  1590  prid1g  4696  isso2i  5538  mpo0v  7359  0wdom  9329  nneo  12404  mnfltpnf  12862  bcpasc  14035  isumless  15557  binomfallfaclem2  15750  lcmfunsnlem2lem1  16343  srabaseOLD  20442  sraaddgOLD  20444  sramulrOLD  20446  m2detleib  21780  fctop  22154  cctop  22156  ovoliunnul  24671  vitalilem5  24776  logtayl  25815  bpos1  26431  usgrexmpldifpr  27625  cffldtocusgr  27814  pthdlem2  28136  inindif  30863  disjunsn  30933  circlemethhgt  32623  fmla0disjsuc  33360  0slt1s  34023  ifpimimb  41111  ifpimim  41116  binomcxplemnn0  41967  binomcxplemnotnn0  41974  salexct  43873  onenotinotbothi  44428  twonotinotbothi  44429  clifte  44430  cliftet  44431  paireqne  44963  sbgoldbo  45239  zlmodzxzldeplem  45839  ldepslinc  45850  line2x  46100  inlinecirc02plem  46132  alimp-surprise  46484  aacllem  46505