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  9289  nn1gt1  9340  nneoor  9752  mnfltpnf  10197  bcpasc  11218  bpos1  16208  usgrexmpldifpr  16588  1loopgruspgr  16642  dceqnconst  17208  nconstwlpolem0  17211