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  4721  isso2i  5600  mpo0v  7527  0wdom  9591  nneo  12810  mnfltpnf  13282  bcpasc  14492  isumless  16043  binomfallfaclem2  16235  lcmfunsnlem2lem1  16842  degenmgm  19166  degenmgm2  19169  m2detleib  22976  fctop  23352  cctop  23354  ovoliunnul  25858  vitalilem5  25963  logtayl  27018  bpos1  27640  0lt1s  28228  n0s0suc  28758  n0s0m1  28778  nn1m1nns  28790  n0seo  28837  usgrexmpldifpr  29869  cffldtocusgr  30058  pthdlem2  30384  disjunsn  33260  circlemethhgt  35342  fmla0disjsuc  36330  disjressuc2  39535  ifpimimb  44697  ifpimim  44702  binomcxplemnn0  45525  binomcxplemnotnn0  45532  salexct  47549  onenotinotbothi  48208  twonotinotbothi  48209  clifte  48210  cliftet  48211  paireqne  48798  sbgoldbo  49090  usgrexmpl1lem  49324  usgrexmpl1tri  49328  usgrexmpl2lem  49329  usgrexmpl2nb0  49334  usgrexmpl2nb1  49335  usgrexmpl2nb2  49336  usgrexmpl2nb3  49337  usgrexmpl2nb4  49338  usgrexmpl2nb5  49339  gpgedg2ov  49369  gpgedg2iv  49370  gpg5nbgrvtx03starlem1  49371  gpg5nbgrvtx03starlem2  49372  gpg5nbgrvtx03starlem3  49373  gpg5nbgrvtx13starlem1  49374  gpg5nbgrvtx13starlem2  49375  gpg5nbgrvtx13starlem3  49376  gpgprismgr4cycllem2  49399  gpgprismgr4cycllem7  49404  gpg5edgnedg  49433  zlmodzxzldeplem  49815  ldepslinc  49826  alimp-surprise  51156  aacllem  51219