Theorem orci 738

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

Syntax hints:   \/ wo 715

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1450  prid1g  3775  onsucelsucexmidlem1  4626  regexmidlemm  4630  nn0suc  4702  nndceq0  4716  0elnn  4717  acexmidlem2  6014  dcfi  7179  exmidaclem  7422  indpi  7561  sup3exmid  9136  nn1gt1  9176  nneoor  9581  mnfltpnf  10019  bcpasc  11027  usgrexmpldifpr  16099  1loopgruspgr  16153  dceqnconst  16664  nconstwlpolem0  16667