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  4513  finexdc  7092  elssdc  7094  finomni  7339  indpi  7562  1ap0  8770  iap0  9367  pnf0xnn0  9472  bcn1  11020  sum0  11950  prod0  12147  odd2np1lem  12434  lcm0val  12638  usgrexmpldifpr  16102  ex-or  16321  dcapnconst  16668