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  3779  onsucelsucexmidlem1  4632  regexmidlemm  4636  nn0suc  4708  nndceq0  4722  0elnn  4723  acexmidlem2  6025  dcfi  7223  exmidaclem  7466  indpi  7605  sup3exmid  9179  nn1gt1  9219  nneoor  9626  mnfltpnf  10064  bcpasc  11074  usgrexmpldifpr  16173  1loopgruspgr  16227  dceqnconst  16776  nconstwlpolem0  16779