Theorem olci 739

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 718	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ∨ 𝜑)

Syntax hints:   ∨ wo 715

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  falortru  1451  sucidg  4515  finexdc  7097  elssdc  7099  finomni  7344  indpi  7567  1ap0  8775  iap0  9372  pnf0xnn0  9477  bcn1  11026  sum0  11972  prod0  12169  odd2np1lem  12456  lcm0val  12660  usgrexmpldifpr  16129  konigsberglem1  16368  ex-or  16375  dcapnconst  16733