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  4539  finexdc  7162  elssdc  7164  fissfi  7218  finomni  7433  indpi  7662  1ap0  8869  iap0  9466  pnf0xnn0  9575  bcn1  11128  sum0  12082  prod0  12279  odd2np1lem  12566  lcm0val  12770  ballotfilemcdc  13150  usgrexmpldifpr  16293  konigsberglem1  16532  ex-or  16539  dcapnconst  16896