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  3727  onsucelsucexmidlem1  4565  regexmidlemm  4569  nn0suc  4641  nndceq0  4655  0elnn  4656  acexmidlem2  5922  dcfi  7056  exmidaclem  7291  indpi  7426  sup3exmid  9001  nn1gt1  9041  nneoor  9445  mnfltpnf  9877  bcpasc  10875  dceqnconst  15791  nconstwlpolem0  15794