Theorem orci 732

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

Syntax hints:   ∨ wo 709

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1417  prid1g  3722  onsucelsucexmidlem1  4560  regexmidlemm  4564  nn0suc  4636  nndceq0  4650  0elnn  4651  acexmidlem2  5915  dcfi  7040  exmidaclem  7268  indpi  7402  sup3exmid  8976  nn1gt1  9016  nneoor  9419  mnfltpnf  9851  bcpasc  10837  dceqnconst  15550  nconstwlpolem0  15553