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 ⊢ (𝜑 ∨ 𝜓)

Syntax hints:   ∨ wo 720

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1455  prid1g  3814  onsucelsucexmidlem1  4673  regexmidlemm  4677  nn0suc  4749  nndceq0  4763  0elnn  4764  acexmidlem2  6076  dcfi  7309  exmidaclem  7558  indpi  7703  sup3exmid  9281  nn1gt1  9321  nneoor  9731  mnfltpnf  10170  bcpasc  11187  usgrexmpldifpr  16473  1loopgruspgr  16527  dceqnconst  17084  nconstwlpolem0  17087