Theorem orci 879

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

This proof depends on syntax axioms:   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  truorfal  1607  prid1g  4717  isso2i  5595  mpo0v  7504  0wdom  9567  nneo  12786  mnfltpnf  13258  bcpasc  14468  isumless  16019  binomfallfaclem2  16211  lcmfunsnlem2lem1  16818  degenmgm  19142  degenmgm2  19145  m2detleib  22951  fctop  23327  cctop  23329  ovoliunnul  25833  vitalilem5  25938  logtayl  26993  bpos1  27615  0lt1s  28203  n0s0suc  28733  n0s0m1  28753  nn1m1nns  28765  n0seo  28812  usgrexmpldifpr  29844  cffldtocusgr  30033  pthdlem2  30359  disjunsn  33235  circlemethhgt  35318  fmla0disjsuc  36249  disjressuc2  39436  ifpimimb  44598  ifpimim  44603  binomcxplemnn0  45426  binomcxplemnotnn0  45433  salexct  47437  onenotinotbothi  48096  twonotinotbothi  48097  clifte  48098  cliftet  48099  paireqne  48686  sbgoldbo  48978  usgrexmpl1lem  49212  usgrexmpl1tri  49216  usgrexmpl2lem  49217  usgrexmpl2nb0  49222  usgrexmpl2nb1  49223  usgrexmpl2nb2  49224  usgrexmpl2nb3  49225  usgrexmpl2nb4  49226  usgrexmpl2nb5  49227  gpgedg2ov  49257  gpgedg2iv  49258  gpg5nbgrvtx03starlem1  49259  gpg5nbgrvtx03starlem2  49260  gpg5nbgrvtx03starlem3  49261  gpg5nbgrvtx13starlem1  49262  gpg5nbgrvtx13starlem2  49263  gpg5nbgrvtx13starlem3  49264  gpgprismgr4cycllem2  49287  gpgprismgr4cycllem7  49292  gpg5edgnedg  49321  zlmodzxzldeplem  49703  ldepslinc  49714  alimp-surprise  51044  aacllem  51107