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 )

This proof depends on syntax axioms:   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  truorfal  1455  prid1g  3815  onsucelsucexmidlem1  4677  regexmidlemm  4681  nn0suc  4753  nndceq0  4767  0elnn  4768  acexmidlem2  6085  dcfi  7320  exmidaclem  7570  indpi  7715  sup3exmid  9295  nn1gt1  9347  nneoor  9758  mnfltpnf  10203  bcpasc  11225  bpos1  16327  usgrexmpldifpr  16712  1loopgruspgr  16766  dceqnconst  17334  nconstwlpolem0  17337