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  3714  onsucelsucexmidlem1  4548  regexmidlemm  4552  nn0suc  4624  nndceq0  4638  0elnn  4639  acexmidlem2  5897  dcfi  7014  exmidaclem  7242  indpi  7376  sup3exmid  8950  nn1gt1  8989  nneoor  9391  mnfltpnf  9822  bcpasc  10788  dceqnconst  15314  nconstwlpolem0  15317