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  4736  isso2i  5598  mpo0v  7491  0wdom  9584  nneo  12677  mnfltpnf  13142  bcpasc  14339  isumless  15861  binomfallfaclem2  16056  lcmfunsnlem2lem1  16657  m2detleib  22569  fctop  22942  cctop  22944  ovoliunnul  25460  vitalilem5  25565  logtayl  26621  bpos1  27246  0slt1s  27793  n0s0suc  28286  n0s0m1  28304  nn1m1nns  28315  n0seo  28359  usgrexmpldifpr  29237  cffldtocusgr  29426  cffldtocusgrOLD  29427  pthdlem2  29750  disjunsn  32575  circlemethhgt  34675  fmla0disjsuc  35420  disjressuc2  38406  ifpimimb  43528  ifpimim  43533  binomcxplemnn0  44373  binomcxplemnotnn0  44380  salexct  46363  onenotinotbothi  46962  twonotinotbothi  46963  clifte  46964  cliftet  46965  paireqne  47525  sbgoldbo  47801  usgrexmpl1lem  48025  usgrexmpl1tri  48029  usgrexmpl2lem  48030  usgrexmpl2nb0  48035  usgrexmpl2nb1  48036  usgrexmpl2nb2  48037  usgrexmpl2nb3  48038  usgrexmpl2nb4  48039  usgrexmpl2nb5  48040  gpg5nbgrvtx03starlem1  48070  gpg5nbgrvtx03starlem2  48071  gpg5nbgrvtx03starlem3  48072  gpg5nbgrvtx13starlem1  48073  gpg5nbgrvtx13starlem2  48074  gpg5nbgrvtx13starlem3  48075  gpgprismgr4cycllem2  48095  gpgprismgr4cycllem7  48100  zlmodzxzldeplem  48474  ldepslinc  48485  line2x  48734  inlinecirc02plem  48766  alimp-surprise  49644  aacllem  49665