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  7564  indpi  7709  sup3exmid  9287  nn1gt1  9338  nneoor  9748  mnfltpnf  10187  bcpasc  11204  usgrexmpldifpr  16490  1loopgruspgr  16544  dceqnconst  17110  nconstwlpolem0  17113