Theorem orci 721

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

Syntax hints:   \/ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  truorfal  1385  prid1g  3635  onsucelsucexmidlem1  4451  regexmidlemm  4455  nn0suc  4526  nndceq0  4539  0elnn  4540  acexmidlem2  5779  exmidaclem  7081  indpi  7174  sup3exmid  8739  nn1gt1  8778  nneoor  9177  mnfltpnf  9601  bcpasc  10544  dceqnconst  13423