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  4677  regexmidlemm  4681  nn0suc  4753  nndceq0  4767  0elnn  4768  acexmidlem2  6085  dcfi  7321  exmidaclem  7571  indpi  7716  sup3exmid  9296  nn1gt1  9348  nneoor  9760  mnfltpnf  10205  bcpasc  11227  bpos1  16322  usgrexmpldifpr  16707  1loopgruspgr  16761  dceqnconst  17329  nconstwlpolem0  17332