Theorem orci 743

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

This proof depends on syntax axioms:   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  truorfal  1455  prid1g  3815  onsucelsucexmidlem1  4675  regexmidlemm  4679  nn0suc  4751  nndceq0  4765  0elnn  4766  acexmidlem2  6082  dcfi  7315  exmidaclem  7564  indpi  7709  sup3exmid  9288  nn1gt1  9339  nneoor  9750  mnfltpnf  10189  bcpasc  11206  usgrexmpldifpr  16502  1loopgruspgr  16556  dceqnconst  17122  nconstwlpolem0  17125