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

Proof of Theorem orci

Step	Hyp	Ref	Expression
1		orci.1	. 2 ⊢ 𝜑
2		orc 720	. 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-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1451  prid1g  3794  onsucelsucexmidlem1  4649  regexmidlemm  4653  nn0suc  4725  nndceq0  4739  0elnn  4740  acexmidlem2  6046  dcfi  7267  exmidaclem  7514  indpi  7653  sup3exmid  9227  nn1gt1  9267  nneoor  9676  mnfltpnf  10114  bcpasc  11124  usgrexmpldifpr  16231  1loopgruspgr  16285  dceqnconst  16832  nconstwlpolem0  16835