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  9759  mnfltpnf  10204  bcpasc  11226  bpos1  16310  usgrexmpldifpr  16695  1loopgruspgr  16749  dceqnconst  17317  nconstwlpolem0  17320