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

Assertion

Ref	Expression
olci	⊢ (𝜓 ∨ 𝜑)

Proof of Theorem olci

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

Syntax hints:   ∨ wo 720

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  falortru  1456  sucidg  4559  finexdc  7201  elssdc  7203  fissfi  7257  finomni  7474  indpi  7703  1ap0  8912  iap0  9511  pnf0xnn0  9620  bcn1  11179  sum0  12138  prod0  12335  odd2np1lem  12622  lcm0val  12826  ballotfilemcdc  13206  usgrexmpldifpr  16473  konigsberglem1  16712  ex-or  16719  dcapnconst  17085