Theorem orci 733

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

Syntax hints:   ∨ wo 710

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1426  prid1g  3738  onsucelsucexmidlem1  4580  regexmidlemm  4584  nn0suc  4656  nndceq0  4670  0elnn  4671  acexmidlem2  5948  dcfi  7090  exmidaclem  7327  indpi  7462  sup3exmid  9037  nn1gt1  9077  nneoor  9482  mnfltpnf  9914  bcpasc  10918  dceqnconst  16073  nconstwlpolem0  16076