Theorem orci 736

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

Syntax hints:   \/ wo 713

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1448  prid1g  3770  onsucelsucexmidlem1  4620  regexmidlemm  4624  nn0suc  4696  nndceq0  4710  0elnn  4711  acexmidlem2  6004  dcfi  7159  exmidaclem  7401  indpi  7540  sup3exmid  9115  nn1gt1  9155  nneoor  9560  mnfltpnf  9993  bcpasc  11000  dceqnconst  16488  nconstwlpolem0  16491