Theorem olci 740

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 719	. 2 |- ( ph -> ( ps \/ ph ) )
3	1, 2	ax-mp 5	1 |- ( ps \/ ph )

Syntax hints:   \/ wo 716

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  falortru  1452  sucidg  4537  finexdc  7160  elssdc  7162  fissfi  7216  finomni  7431  indpi  7657  1ap0  8864  iap0  9461  pnf0xnn0  9570  bcn1  11120  sum0  12074  prod0  12271  odd2np1lem  12558  lcm0val  12762  usgrexmpldifpr  16244  konigsberglem1  16483  ex-or  16490  dcapnconst  16847