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  4519  finexdc  7135  elssdc  7137  finomni  7382  indpi  7605  1ap0  8812  iap0  9409  pnf0xnn0  9516  bcn1  11066  sum0  12012  prod0  12209  odd2np1lem  12496  lcm0val  12700  usgrexmpldifpr  16173  konigsberglem1  16412  ex-or  16419  dcapnconst  16777