Theorem orci 878

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 151	. 2 ⊢ (¬ 𝜑 → 𝜓)
3	2	orri 875	1 ⊢ (𝜑 ∨ 𝜓)

Syntax hints:   ∨ wo 860

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 861

This theorem is referenced by:  truorfal  1608  prid1g  4727  isso2i  5608  mpo0v  7496  0wdom  9533  nneo  12681  mnfltpnf  13152  bcpasc  14359  isumless  15901  binomfallfaclem2  16095  lcmfunsnlem2lem1  16697  m2detleib  22769  fctop  23142  cctop  23144  ovoliunnul  25647  vitalilem5  25752  logtayl  26803  bpos1  27425  0lt1s  27983  n0s0suc  28513  n0s0m1  28533  nn1m1nns  28545  n0seo  28592  usgrexmpldifpr  29586  cffldtocusgr  29775  pthdlem2  30095  disjunsn  32917  circlemethhgt  35008  fmla0disjsuc  35868  disjressuc2  39038  ifpimimb  44210  ifpimim  44215  binomcxplemnn0  45039  binomcxplemnotnn0  45046  salexct  47028  onenotinotbothi  47647  twonotinotbothi  47648  clifte  47649  cliftet  47650  paireqne  48237  sbgoldbo  48529  usgrexmpl1lem  48763  usgrexmpl1tri  48767  usgrexmpl2lem  48768  usgrexmpl2nb0  48773  usgrexmpl2nb1  48774  usgrexmpl2nb2  48775  usgrexmpl2nb3  48776  usgrexmpl2nb4  48777  usgrexmpl2nb5  48778  gpgedg2ov  48808  gpgedg2iv  48809  gpg5nbgrvtx03starlem1  48810  gpg5nbgrvtx03starlem2  48811  gpg5nbgrvtx03starlem3  48812  gpg5nbgrvtx13starlem1  48813  gpg5nbgrvtx13starlem2  48814  gpg5nbgrvtx13starlem3  48815  gpgprismgr4cycllem2  48838  gpgprismgr4cycllem7  48843  gpg5edgnedg  48872  zlmodzxzldeplem  49255  ldepslinc  49266  line2x  49511  inlinecirc02plem  49543  alimp-surprise  50535  aacllem  50578