Theorem orci 736

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

Syntax hints:   ∨ wo 713

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1448  prid1g  3773  onsucelsucexmidlem1  4624  regexmidlemm  4628  nn0suc  4700  nndceq0  4714  0elnn  4715  acexmidlem2  6010  dcfi  7174  exmidaclem  7416  indpi  7555  sup3exmid  9130  nn1gt1  9170  nneoor  9575  mnfltpnf  10013  bcpasc  11021  usgrexmpldifpr  16093  1loopgruspgr  16114  dceqnconst  16614  nconstwlpolem0  16617