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  4536  finexdc  7159  elssdc  7161  fissfi  7215  finomni  7430  indpi  7653  1ap0  8860  iap0  9457  pnf0xnn0  9566  bcn1  11116  sum0  12067  prod0  12264  odd2np1lem  12551  lcm0val  12755  usgrexmpldifpr  16231  konigsberglem1  16470  ex-or  16477  dcapnconst  16833