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  1608  prid1g  4731  isso2i  5611  mpo0v  7507  0wdom  9542  nneo  12698  mnfltpnf  13169  bcpasc  14377  isumless  15925  binomfallfaclem2  16119  lcmfunsnlem2lem1  16721  m2detleib  22825  fctop  23198  cctop  23200  ovoliunnul  25703  vitalilem5  25808  logtayl  26862  bpos1  27484  0lt1s  28042  n0s0suc  28572  n0s0m1  28592  nn1m1nns  28604  n0seo  28651  usgrexmpldifpr  29645  cffldtocusgr  29834  pthdlem2  30154  disjunsn  32976  circlemethhgt  35062  fmla0disjsuc  35911  disjressuc2  39101  ifpimimb  44271  ifpimim  44276  binomcxplemnn0  45100  binomcxplemnotnn0  45107  salexct  47089  onenotinotbothi  47711  twonotinotbothi  47712  clifte  47713  cliftet  47714  paireqne  48301  sbgoldbo  48593  usgrexmpl1lem  48827  usgrexmpl1tri  48831  usgrexmpl2lem  48832  usgrexmpl2nb0  48837  usgrexmpl2nb1  48838  usgrexmpl2nb2  48839  usgrexmpl2nb3  48840  usgrexmpl2nb4  48841  usgrexmpl2nb5  48842  gpgedg2ov  48872  gpgedg2iv  48873  gpg5nbgrvtx03starlem1  48874  gpg5nbgrvtx03starlem2  48875  gpg5nbgrvtx03starlem3  48876  gpg5nbgrvtx13starlem1  48877  gpg5nbgrvtx13starlem2  48878  gpg5nbgrvtx13starlem3  48879  gpgprismgr4cycllem2  48902  gpgprismgr4cycllem7  48907  gpg5edgnedg  48936  zlmodzxzldeplem  49319  ldepslinc  49330  line2x  49575  inlinecirc02plem  49607  alimp-surprise  50599  aacllem  50662