Theorem orci 735

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

Syntax hints:   ∨ wo 712

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1428  prid1g  3750  onsucelsucexmidlem1  4597  regexmidlemm  4601  nn0suc  4673  nndceq0  4687  0elnn  4688  acexmidlem2  5971  dcfi  7116  exmidaclem  7358  indpi  7497  sup3exmid  9072  nn1gt1  9112  nneoor  9517  mnfltpnf  9949  bcpasc  10955  dceqnconst  16339  nconstwlpolem0  16342