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  4675  regexmidlemm  4679  nn0suc  4751  nndceq0  4765  0elnn  4766  acexmidlem2  6082  dcfi  7315  exmidaclem  7565  indpi  7710  sup3exmid  9290  nn1gt1  9341  nneoor  9753  mnfltpnf  10198  bcpasc  11220  bpos1  16271  usgrexmpldifpr  16656  1loopgruspgr  16710  dceqnconst  17277  nconstwlpolem0  17280