Theorem orci 871

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

Syntax hints:   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  truorfal  1585  prid1g  4699  isso2i  5570  mpo0v  7447  0wdom  9482  nneo  12611  mnfltpnf  13075  bcpasc  14281  isumless  15808  binomfallfaclem2  16003  lcmfunsnlem2lem1  16605  m2detleib  22621  fctop  22994  cctop  22996  ovoliunnul  25499  vitalilem5  25604  logtayl  26649  bpos1  27271  0lt1s  27829  n0s0suc  28359  n0s0m1  28379  nn1m1nns  28391  n0seo  28438  usgrexmpldifpr  29352  cffldtocusgr  29541  pthdlem2  29861  disjunsn  32690  circlemethhgt  34834  fmla0disjsuc  35633  disjressuc2  38785  ifpimimb  43955  ifpimim  43960  binomcxplemnn0  44800  binomcxplemnotnn0  44807  salexct  46784  onenotinotbothi  47403  twonotinotbothi  47404  clifte  47405  cliftet  47406  paireqne  47993  sbgoldbo  48285  usgrexmpl1lem  48519  usgrexmpl1tri  48523  usgrexmpl2lem  48524  usgrexmpl2nb0  48529  usgrexmpl2nb1  48530  usgrexmpl2nb2  48531  usgrexmpl2nb3  48532  usgrexmpl2nb4  48533  usgrexmpl2nb5  48534  gpgedg2ov  48564  gpgedg2iv  48565  gpg5nbgrvtx03starlem1  48566  gpg5nbgrvtx03starlem2  48567  gpg5nbgrvtx03starlem3  48568  gpg5nbgrvtx13starlem1  48569  gpg5nbgrvtx13starlem2  48570  gpg5nbgrvtx13starlem3  48571  gpgprismgr4cycllem2  48594  gpgprismgr4cycllem7  48599  gpg5edgnedg  48628  zlmodzxzldeplem  48996  ldepslinc  49007  line2x  49252  inlinecirc02plem  49284  alimp-surprise  50277  aacllem  50298