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  1601  prid1g  4722  isso2i  5597  mpo0v  7484  0wdom  9520  nneo  12671  mnfltpnf  13142  bcpasc  14348  isumless  15889  binomfallfaclem2  16084  lcmfunsnlem2lem1  16686  m2detleib  22749  fctop  23122  cctop  23124  ovoliunnul  25627  vitalilem5  25732  logtayl  26783  bpos1  27405  0lt1s  27963  n0s0suc  28493  n0s0m1  28513  nn1m1nns  28525  n0seo  28572  usgrexmpldifpr  29517  cffldtocusgr  29706  pthdlem2  30026  disjunsn  32849  circlemethhgt  34947  fmla0disjsuc  35761  disjressuc2  38922  ifpimimb  44092  ifpimim  44097  binomcxplemnn0  44923  binomcxplemnotnn0  44930  salexct  46906  onenotinotbothi  47525  twonotinotbothi  47526  clifte  47527  cliftet  47528  paireqne  48115  sbgoldbo  48407  usgrexmpl1lem  48641  usgrexmpl1tri  48645  usgrexmpl2lem  48646  usgrexmpl2nb0  48651  usgrexmpl2nb1  48652  usgrexmpl2nb2  48653  usgrexmpl2nb3  48654  usgrexmpl2nb4  48655  usgrexmpl2nb5  48656  gpgedg2ov  48686  gpgedg2iv  48687  gpg5nbgrvtx03starlem1  48688  gpg5nbgrvtx03starlem2  48689  gpg5nbgrvtx03starlem3  48690  gpg5nbgrvtx13starlem1  48691  gpg5nbgrvtx13starlem2  48692  gpg5nbgrvtx13starlem3  48693  gpgprismgr4cycllem2  48716  gpgprismgr4cycllem7  48721  gpg5edgnedg  48750  zlmodzxzldeplem  49129  ldepslinc  49140  line2x  49385  inlinecirc02plem  49417  alimp-surprise  50409  aacllem  50430