Theorem orci 405

Description: Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)

Hypothesis

Ref	Expression
orci.1	|- ph

Assertion

Ref	Expression
orci	|- ( ph \/ ps )

Proof of Theorem orci

Step	Hyp	Ref	Expression
1		orci.1	. . 3 |- ph
2	1	pm2.24i 146	. 2 |- ( -. ph -> ps )
3	2	orri 391	1 |- ( ph \/ ps )

Syntax hints:   \/ wo 383

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 197  df-or 385

This theorem is referenced by:  truorfal  1511  prid1g  4295  isso2i  5067  0wdom  8475  nneo  11461  mnfltpnf  11960  bcpasc  13108  isumless  14577  binomfallfaclem2  14771  lcmfunsnlem2lem1  15351  srabase  19178  sraaddg  19179  sramulr  19180  m2detleib  20437  fctop  20808  cctop  20810  ovoliunnul  23275  vitalilem5  23381  logtayl  24406  bpos1  25008  usgrexmpldifpr  26150  cffldtocusgr  26343  pthdlem2  26664  inindif  29353  disjunsn  29407  circlemethhgt  30721  ifpimimb  37849  ifpimim  37854  binomcxplemnn0  38548  binomcxplemnotnn0  38555  salexct  40552  onenotinotbothi  41100  twonotinotbothi  41101  clifte  41102  cliftet  41103  sbgoldbo  41675  zlmodzxzldeplem  42287  ldepslinc  42298  alimp-surprise  42526  aacllem  42547