Theorem olci 737

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

Syntax hints:   ∨ wo 713

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  falortru  1449  sucidg  4508  finexdc  7078  elssdc  7080  finomni  7323  indpi  7545  1ap0  8753  iap0  9350  pnf0xnn0  9455  bcn1  10997  sum0  11920  prod0  12117  odd2np1lem  12404  lcm0val  12608  usgrexmpldifpr  16068  ex-or  16195  dcapnconst  16543