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  4724  isso2i  5604  mpo0v  7501  0wdom  9546  nneo  12709  mnfltpnf  13181  bcpasc  14389  isumless  15938  binomfallfaclem2  16132  lcmfunsnlem2lem1  16734  degenmgm  19056  degenmgm2  19059  m2detleib  22859  fctop  23235  cctop  23237  ovoliunnul  25741  vitalilem5  25846  logtayl  26905  bpos1  27527  0lt1s  28085  n0s0suc  28615  n0s0m1  28635  nn1m1nns  28647  n0seo  28694  usgrexmpldifpr  29726  cffldtocusgr  29915  pthdlem2  30241  disjunsn  33075  circlemethhgt  35159  fmla0disjsuc  35985  disjressuc2  39167  ifpimimb  44352  ifpimim  44357  binomcxplemnn0  45181  binomcxplemnotnn0  45188  salexct  47170  onenotinotbothi  47829  twonotinotbothi  47830  clifte  47831  cliftet  47832  paireqne  48419  sbgoldbo  48711  usgrexmpl1lem  48945  usgrexmpl1tri  48949  usgrexmpl2lem  48950  usgrexmpl2nb0  48955  usgrexmpl2nb1  48956  usgrexmpl2nb2  48957  usgrexmpl2nb3  48958  usgrexmpl2nb4  48959  usgrexmpl2nb5  48960  gpgedg2ov  48990  gpgedg2iv  48991  gpg5nbgrvtx03starlem1  48992  gpg5nbgrvtx03starlem2  48993  gpg5nbgrvtx03starlem3  48994  gpg5nbgrvtx13starlem1  48995  gpg5nbgrvtx13starlem2  48996  gpg5nbgrvtx13starlem3  48997  gpgprismgr4cycllem2  49020  gpgprismgr4cycllem7  49025  gpg5edgnedg  49054  zlmodzxzldeplem  49436  ldepslinc  49447  line2x  49692  inlinecirc02plem  49724  alimp-surprise  50717  aacllem  50780