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  1417  prid1g  3723  onsucelsucexmidlem1  4561  regexmidlemm  4565  nn0suc  4637  nndceq0  4651  0elnn  4652  acexmidlem2  5916  dcfi  7042  exmidaclem  7270  indpi  7404  sup3exmid  8978  nn1gt1  9018  nneoor  9422  mnfltpnf  9854  bcpasc  10840  dceqnconst  15620  nconstwlpolem0  15623