Theorem orci 743

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

Syntax hints:   \/ wo 720

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1455  prid1g  3811  onsucelsucexmidlem1  4670  regexmidlemm  4674  nn0suc  4746  nndceq0  4760  0elnn  4761  acexmidlem2  6072  dcfi  7305  exmidaclem  7554  indpi  7699  sup3exmid  9277  nn1gt1  9317  nneoor  9727  mnfltpnf  10166  bcpasc  11182  usgrexmpldifpr  16404  1loopgruspgr  16458  dceqnconst  17015  nconstwlpolem0  17018