Theorem orci 731

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

Syntax hints:   \/ wo 708

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1406  prid1g  3696  onsucelsucexmidlem1  4527  regexmidlemm  4531  nn0suc  4603  nndceq0  4617  0elnn  4618  acexmidlem2  5871  dcfi  6979  exmidaclem  7206  indpi  7340  sup3exmid  8912  nn1gt1  8951  nneoor  9353  mnfltpnf  9783  bcpasc  10741  dceqnconst  14689  nconstwlpolem0  14692