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  3773  onsucelsucexmidlem1  4624  regexmidlemm  4628  nn0suc  4700  nndceq0  4714  0elnn  4715  acexmidlem2  6010  dcfi  7171  exmidaclem  7413  indpi  7552  sup3exmid  9127  nn1gt1  9167  nneoor  9572  mnfltpnf  10010  bcpasc  11018  usgrexmpldifpr  16088  1loopgruspgr  16109  dceqnconst  16600  nconstwlpolem0  16603