Theorem orci 732

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

Syntax hints:   \/ wo 709

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1425  prid1g  3736  onsucelsucexmidlem1  4575  regexmidlemm  4579  nn0suc  4651  nndceq0  4665  0elnn  4666  acexmidlem2  5940  dcfi  7082  exmidaclem  7319  indpi  7454  sup3exmid  9029  nn1gt1  9069  nneoor  9474  mnfltpnf  9906  bcpasc  10909  dceqnconst  15932  nconstwlpolem0  15935