Theorem orci 863

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 150	. 2 ⊢ (¬ 𝜑 → 𝜓)
3	2	orri 860	1 ⊢ (𝜑 ∨ 𝜓)

Syntax hints:   ∨ wo 845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-or 846

This theorem is referenced by:  truorfal  1579  prid1g  4763  isso2i  5622  mpo0v  7489  0wdom  9561  nneo  12642  mnfltpnf  13102  bcpasc  14277  isumless  15787  binomfallfaclem2  15980  lcmfunsnlem2lem1  16571  srabaseOLD  20785  sraaddgOLD  20787  sramulrOLD  20789  m2detleib  22124  fctop  22498  cctop  22500  ovoliunnul  25015  vitalilem5  25120  logtayl  26159  bpos1  26775  0slt1s  27319  usgrexmpldifpr  28504  cffldtocusgr  28693  pthdlem2  29014  inindif  31741  disjunsn  31812  circlemethhgt  33643  fmla0disjsuc  34377  disjressuc2  37246  ifpimimb  42240  ifpimim  42245  binomcxplemnn0  43093  binomcxplemnotnn0  43100  salexct  45036  onenotinotbothi  45629  twonotinotbothi  45630  clifte  45631  cliftet  45632  paireqne  46165  sbgoldbo  46441  zlmodzxzldeplem  47132  ldepslinc  47143  line2x  47393  inlinecirc02plem  47425  alimp-surprise  47780  aacllem  47801