Theorem orci 739

Description: Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Revised by Mario Carneiro, 31-Jan-2015.)

Hypothesis

Ref	Expression
orci.1	|- ph

Assertion

Ref	Expression
orci	|- ( ph \/ ps )

Proof of Theorem orci

Step	Hyp	Ref	Expression
1		orci.1	. 2 |- ph
2		orc 720	. 2 |- ( ph -> ( ph \/ ps ) )
3	1, 2	ax-mp 5	1 |- ( ph \/ ps )

Syntax hints:   \/ wo 716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1451  prid1g  3795  onsucelsucexmidlem1  4650  regexmidlemm  4654  nn0suc  4726  nndceq0  4740  0elnn  4741  acexmidlem2  6047  dcfi  7268  exmidaclem  7515  indpi  7657  sup3exmid  9231  nn1gt1  9271  nneoor  9680  mnfltpnf  10118  bcpasc  11128  usgrexmpldifpr  16244  1loopgruspgr  16298  dceqnconst  16846  nconstwlpolem0  16849