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	⊢ 𝜑

Assertion

Ref	Expression
olci	⊢ (𝜓 ∨ 𝜑)

Proof of Theorem olci

Step	Hyp	Ref	Expression
1		orci.1	. 2 ⊢ 𝜑
2		olc 719	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ∨ 𝜑)

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  4542  finexdc  7173  elssdc  7175  fissfi  7229  finomni  7444  indpi  7673  1ap0  8882  iap0  9481  pnf0xnn0  9590  bcn1  11148  sum0  12102  prod0  12299  odd2np1lem  12586  lcm0val  12790  ballotfilemcdc  13170  usgrexmpldifpr  16373  konigsberglem1  16612  ex-or  16619  dcapnconst  16986