Theorem orci 866

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

Syntax hints:   ∨ wo 848

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 849

This theorem is referenced by:  truorfal  1580  prid1g  4705  isso2i  5569  mpo0v  7444  0wdom  9478  nneo  12604  mnfltpnf  13068  bcpasc  14274  isumless  15801  binomfallfaclem2  15996  lcmfunsnlem2lem1  16598  m2detleib  22606  fctop  22979  cctop  22981  ovoliunnul  25484  vitalilem5  25589  logtayl  26637  bpos1  27260  0lt1s  27818  n0s0suc  28348  n0s0m1  28368  nn1m1nns  28380  n0seo  28427  usgrexmpldifpr  29341  cffldtocusgr  29530  cffldtocusgrOLD  29531  pthdlem2  29851  disjunsn  32679  circlemethhgt  34803  fmla0disjsuc  35596  disjressuc2  38746  ifpimimb  43949  ifpimim  43954  binomcxplemnn0  44794  binomcxplemnotnn0  44801  salexct  46780  onenotinotbothi  47393  twonotinotbothi  47394  clifte  47395  cliftet  47396  paireqne  47983  sbgoldbo  48275  usgrexmpl1lem  48509  usgrexmpl1tri  48513  usgrexmpl2lem  48514  usgrexmpl2nb0  48519  usgrexmpl2nb1  48520  usgrexmpl2nb2  48521  usgrexmpl2nb3  48522  usgrexmpl2nb4  48523  usgrexmpl2nb5  48524  gpgedg2ov  48554  gpgedg2iv  48555  gpg5nbgrvtx03starlem1  48556  gpg5nbgrvtx03starlem2  48557  gpg5nbgrvtx03starlem3  48558  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem2  48560  gpg5nbgrvtx13starlem3  48561  gpgprismgr4cycllem2  48584  gpgprismgr4cycllem7  48589  gpg5edgnedg  48618  zlmodzxzldeplem  48986  ldepslinc  48997  line2x  49242  inlinecirc02plem  49274  alimp-surprise  50267  aacllem  50288