Theorem orci 738

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

Syntax hints:   ∨ wo 715

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1450  prid1g  3775  onsucelsucexmidlem1  4626  regexmidlemm  4630  nn0suc  4702  nndceq0  4716  0elnn  4717  acexmidlem2  6015  dcfi  7180  exmidaclem  7423  indpi  7562  sup3exmid  9137  nn1gt1  9177  nneoor  9582  mnfltpnf  10020  bcpasc  11029  usgrexmpldifpr  16103  1loopgruspgr  16157  dceqnconst  16685  nconstwlpolem0  16688