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  5596  mpo0v  7496  0wdom  9548  nneo  12764  mnfltpnf  13236  bcpasc  14445  isumless  15994  binomfallfaclem2  16186  lcmfunsnlem2lem1  16793  degenmgm  19117  degenmgm2  19120  m2detleib  22926  fctop  23302  cctop  23304  ovoliunnul  25808  vitalilem5  25913  logtayl  26970  bpos1  27592  0lt1s  28180  n0s0suc  28710  n0s0m1  28730  nn1m1nns  28742  n0seo  28789  usgrexmpldifpr  29821  cffldtocusgr  30010  pthdlem2  30336  disjunsn  33170  circlemethhgt  35255  fmla0disjsuc  36132  disjressuc2  39311  ifpimimb  44463  ifpimim  44468  binomcxplemnn0  45292  binomcxplemnotnn0  45299  salexct  47288  onenotinotbothi  47947  twonotinotbothi  47948  clifte  47949  cliftet  47950  paireqne  48537  sbgoldbo  48829  usgrexmpl1lem  49063  usgrexmpl1tri  49067  usgrexmpl2lem  49068  usgrexmpl2nb0  49073  usgrexmpl2nb1  49074  usgrexmpl2nb2  49075  usgrexmpl2nb3  49076  usgrexmpl2nb4  49077  usgrexmpl2nb5  49078  gpgedg2ov  49108  gpgedg2iv  49109  gpg5nbgrvtx03starlem1  49110  gpg5nbgrvtx03starlem2  49111  gpg5nbgrvtx03starlem3  49112  gpg5nbgrvtx13starlem1  49113  gpg5nbgrvtx13starlem2  49114  gpg5nbgrvtx13starlem3  49115  gpgprismgr4cycllem2  49138  gpgprismgr4cycllem7  49143  gpg5edgnedg  49172  zlmodzxzldeplem  49554  ldepslinc  49565  line2x  49810  inlinecirc02plem  49842  alimp-surprise  50820  aacllem  50883