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  3797  onsucelsucexmidlem1  4652  regexmidlemm  4656  nn0suc  4728  nndceq0  4742  0elnn  4743  acexmidlem2  6049  dcfi  7270  exmidaclem  7517  indpi  7662  sup3exmid  9236  nn1gt1  9276  nneoor  9686  mnfltpnf  10124  bcpasc  11136  usgrexmpldifpr  16293  1loopgruspgr  16347  dceqnconst  16895  nconstwlpolem0  16898