Theorem orci 739

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

Syntax hints:   \/ wo 716

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1451  prid1g  3800  onsucelsucexmidlem1  4655  regexmidlemm  4659  nn0suc  4731  nndceq0  4745  0elnn  4746  acexmidlem2  6055  dcfi  7281  exmidaclem  7528  indpi  7673  sup3exmid  9248  nn1gt1  9288  nneoor  9698  mnfltpnf  10137  bcpasc  11153  usgrexmpldifpr  16370  1loopgruspgr  16424  dceqnconst  16972  nconstwlpolem0  16975