Theorem orci 736

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

Syntax hints:   \/ wo 713

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1448  prid1g  3770  onsucelsucexmidlem1  4619  regexmidlemm  4623  nn0suc  4695  nndceq0  4709  0elnn  4710  acexmidlem2  5997  dcfi  7144  exmidaclem  7386  indpi  7525  sup3exmid  9100  nn1gt1  9140  nneoor  9545  mnfltpnf  9977  bcpasc  10983  dceqnconst  16387  nconstwlpolem0  16390