Theorem orci 733

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 714	. 2 |- ( ph -> ( ph \/ ps ) )
3	1, 2	ax-mp 5	1 |- ( ph \/ ps )

Syntax hints:   \/ wo 710

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1426  prid1g  3742  onsucelsucexmidlem1  4589  regexmidlemm  4593  nn0suc  4665  nndceq0  4679  0elnn  4680  acexmidlem2  5959  dcfi  7104  exmidaclem  7346  indpi  7485  sup3exmid  9060  nn1gt1  9100  nneoor  9505  mnfltpnf  9937  bcpasc  10943  dceqnconst  16171  nconstwlpolem0  16174