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 153	. 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 209  df-or 844

This theorem is referenced by:  truorfal  1575  trunortruOLD  1587  trunorfalOLD  1589  prid1g  4698  isso2i  5510  mpo0v  7240  0wdom  9036  nneo  12069  mnfltpnf  12524  bcpasc  13684  isumless  15202  binomfallfaclem2  15396  lcmfunsnlem2lem1  15984  srabase  19952  sraaddg  19953  sramulr  19954  m2detleib  21242  fctop  21614  cctop  21616  ovoliunnul  24110  vitalilem5  24215  logtayl  25245  bpos1  25861  usgrexmpldifpr  27042  cffldtocusgr  27231  pthdlem2  27551  inindif  30280  disjunsn  30346  circlemethhgt  31916  fmla0disjsuc  32647  ifpimimb  39877  ifpimim  39882  binomcxplemnn0  40688  binomcxplemnotnn0  40695  salexct  42624  onenotinotbothi  43176  twonotinotbothi  43177  clifte  43178  cliftet  43179  paireqne  43680  sbgoldbo  43959  zlmodzxzldeplem  44560  ldepslinc  44571  line2x  44748  inlinecirc02plem  44780  alimp-surprise  44888  aacllem  44909