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  4574  regexmidlemm  4578  nn0suc  4650  nndceq0  4664  0elnn  4665  acexmidlem2  5931  dcfi  7065  exmidaclem  7302  indpi  7437  sup3exmid  9012  nn1gt1  9052  nneoor  9457  mnfltpnf  9889  bcpasc  10892  dceqnconst  15863  nconstwlpolem0  15866