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  3697  onsucelsucexmidlem1  4528  regexmidlemm  4532  nn0suc  4604  nndceq0  4618  0elnn  4619  acexmidlem2  5872  dcfi  6980  exmidaclem  7207  indpi  7341  sup3exmid  8914  nn1gt1  8953  nneoor  9355  mnfltpnf  9785  bcpasc  10746  dceqnconst  14810  nconstwlpolem0  14813