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  1571  trunortruOLD  1583  trunorfalOLD  1585  prid1g  4690  isso2i  5503  mpo0v  7232  0wdom  9028  nneo  12060  mnfltpnf  12515  bcpasc  13675  isumless  15194  binomfallfaclem2  15388  lcmfunsnlem2lem1  15976  srabase  19944  sraaddg  19945  sramulr  19946  m2detleib  21234  fctop  21606  cctop  21608  ovoliunnul  24102  vitalilem5  24207  logtayl  25237  bpos1  25853  usgrexmpldifpr  27034  cffldtocusgr  27223  pthdlem2  27543  inindif  30272  disjunsn  30338  circlemethhgt  31909  fmla0disjsuc  32640  ifpimimb  39863  ifpimim  39868  binomcxplemnn0  40674  binomcxplemnotnn0  40681  salexct  42610  onenotinotbothi  43162  twonotinotbothi  43163  clifte  43164  cliftet  43165  paireqne  43666  sbgoldbo  43945  zlmodzxzldeplem  44546  ldepslinc  44557  line2x  44734  inlinecirc02plem  44766  alimp-surprise  44874  aacllem  44895