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 ⊢ (𝜓 ∨ 𝜑)

This proof depends on syntax axioms:   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  falortru  1456  sucidg  4563  finexdc  7212  elssdc  7214  fissfi  7268  finomni  7487  indpi  7716  1ap0  8927  iap0  9540  pnf0xnn0  9649  bcn1  11219  sum0  12181  prod0  12378  odd2np1lem  12665  lcm0val  12869  ballotfilemcdc  13282  bpos1  16322  usgrexmpldifpr  16707  konigsberglem1  16946  ex-or  16953  dcapnconst  17330