Theorem orci 726

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

Syntax hints:   \/ wo 703

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  truorfal  1401  prid1g  3687  onsucelsucexmidlem1  4512  regexmidlemm  4516  nn0suc  4588  nndceq0  4602  0elnn  4603  acexmidlem2  5850  dcfi  6958  exmidaclem  7185  indpi  7304  sup3exmid  8873  nn1gt1  8912  nneoor  9314  mnfltpnf  9742  bcpasc  10700  dceqnconst  14091  nconstwlpolem0  14094