Theorem olci 744

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
olci	|- ( ps \/ ph )

Proof of Theorem olci

Step	Hyp	Ref	Expression
1		orci.1	. 2 |- ph
2		olc 723	. 2 |- ( ph -> ( ps \/ ph ) )
3	1, 2	ax-mp 5	1 |- ( ps \/ ph )

Syntax hints:   \/ wo 720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-io 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  falortru  1456  sucidg  4556  finexdc  7197  elssdc  7199  fissfi  7253  finomni  7470  indpi  7699  1ap0  8908  iap0  9507  pnf0xnn0  9616  bcn1  11174  sum0  12133  prod0  12330  odd2np1lem  12617  lcm0val  12821  ballotfilemcdc  13201  usgrexmpldifpr  16404  konigsberglem1  16643  ex-or  16650  dcapnconst  17016