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  3776  onsucelsucexmidlem1  4628  regexmidlemm  4632  nn0suc  4704  nndceq0  4718  0elnn  4719  acexmidlem2  6020  dcfi  7185  exmidaclem  7428  indpi  7567  sup3exmid  9142  nn1gt1  9182  nneoor  9587  mnfltpnf  10025  bcpasc  11034  usgrexmpldifpr  16129  1loopgruspgr  16183  dceqnconst  16732  nconstwlpolem0  16735