Theorem orci 739

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

Syntax hints:   ∨ wo 716

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1451  prid1g  3800  onsucelsucexmidlem1  4655  regexmidlemm  4659  nn0suc  4731  nndceq0  4745  0elnn  4746  acexmidlem2  6055  dcfi  7281  exmidaclem  7528  indpi  7673  sup3exmid  9251  nn1gt1  9291  nneoor  9701  mnfltpnf  10140  bcpasc  11156  usgrexmpldifpr  16373  1loopgruspgr  16427  dceqnconst  16985  nconstwlpolem0  16988