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 )

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-ia2 107  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  falortru  1456  sucidg  4563  finexdc  7213  elssdc  7215  fissfi  7269  finomni  7486  indpi  7715  1ap0  8926  iap0  9539  pnf0xnn0  9646  bcn1  11217  sum0  12179  prod0  12376  odd2np1lem  12663  lcm0val  12867  ballotfilemcdc  13280  bpos1  16327  usgrexmpldifpr  16712  konigsberglem1  16951  ex-or  16958  dcapnconst  17335