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  4561  finexdc  7207  elssdc  7209  fissfi  7263  finomni  7481  indpi  7710  1ap0  8921  iap0  9533  pnf0xnn0  9642  bcn1  11212  sum0  12174  prod0  12371  odd2np1lem  12658  lcm0val  12862  ballotfilemcdc  13275  bpos1  16276  usgrexmpldifpr  16661  konigsberglem1  16900  ex-or  16907  dcapnconst  17283