Theorem orci 865

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 862	1 ⊢ (𝜑 ∨ 𝜓)

Syntax hints:   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  truorfal  1578  prid1g  4714  isso2i  5568  mpo0v  7437  0wdom  9481  nneo  12578  mnfltpnf  13046  bcpasc  14246  isumless  15770  binomfallfaclem2  15965  lcmfunsnlem2lem1  16567  m2detleib  22534  fctop  22907  cctop  22909  ovoliunnul  25424  vitalilem5  25529  logtayl  26585  bpos1  27210  0slt1s  27761  n0s0suc  28257  n0s0m1  28275  nn1m1nns  28286  n0seo  28331  usgrexmpldifpr  29221  cffldtocusgr  29410  cffldtocusgrOLD  29411  pthdlem2  29731  disjunsn  32556  circlemethhgt  34610  fmla0disjsuc  35370  disjressuc2  38359  ifpimimb  43477  ifpimim  43482  binomcxplemnn0  44322  binomcxplemnotnn0  44329  salexct  46316  onenotinotbothi  46918  twonotinotbothi  46919  clifte  46920  cliftet  46921  paireqne  47496  sbgoldbo  47772  usgrexmpl1lem  48006  usgrexmpl1tri  48010  usgrexmpl2lem  48011  usgrexmpl2nb0  48016  usgrexmpl2nb1  48017  usgrexmpl2nb2  48018  usgrexmpl2nb3  48019  usgrexmpl2nb4  48020  usgrexmpl2nb5  48021  gpgedg2ov  48051  gpgedg2iv  48052  gpg5nbgrvtx03starlem1  48053  gpg5nbgrvtx03starlem2  48054  gpg5nbgrvtx03starlem3  48055  gpg5nbgrvtx13starlem1  48056  gpg5nbgrvtx13starlem2  48057  gpg5nbgrvtx13starlem3  48058  gpgprismgr4cycllem2  48081  gpgprismgr4cycllem7  48086  gpg5edgnedg  48115  zlmodzxzldeplem  48484  ldepslinc  48495  line2x  48740  inlinecirc02plem  48772  alimp-surprise  49766  aacllem  49787