Theorem orci 732

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

Syntax hints:   \/ wo 709

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1417  prid1g  3726  onsucelsucexmidlem1  4564  regexmidlemm  4568  nn0suc  4640  nndceq0  4654  0elnn  4655  acexmidlem2  5919  dcfi  7047  exmidaclem  7275  indpi  7409  sup3exmid  8984  nn1gt1  9024  nneoor  9428  mnfltpnf  9860  bcpasc  10858  dceqnconst  15704  nconstwlpolem0  15707