Theorem orci 721

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

Syntax hints:   ∨ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  truorfal  1396  prid1g  3680  onsucelsucexmidlem1  4505  regexmidlemm  4509  nn0suc  4581  nndceq0  4595  0elnn  4596  acexmidlem2  5839  dcfi  6946  exmidaclem  7164  indpi  7283  sup3exmid  8852  nn1gt1  8891  nneoor  9293  mnfltpnf  9721  bcpasc  10679  dceqnconst  13938  nconstwlpolem0  13941